X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fdatatypes%2Fbool.ma;h=f4aec8167476b0d88204a06d3d23aaa798a323ac;hb=118769957a508c21b72bd7b9d2dbf64f654fe21c;hp=11f1d7a8c49d48047e12caaeec555c207e1ca784;hpb=8881e203658bb17d37bdea24ea3e104d0466e2e8;p=helm.git

diff --git a/helm/matita/library/datatypes/bool.ma b/helm/matita/library/datatypes/bool.ma
index 11f1d7a8c..f4aec8167 100644
--- a/helm/matita/library/datatypes/bool.ma
+++ b/helm/matita/library/datatypes/bool.ma
@@ -32,7 +32,7 @@ theorem bool_elim: \forall P:bool \to Prop. \forall b:bool.
 qed.
 
 theorem not_eq_true_false : true \neq false.
-simplify.intro.
+unfold Not.intro.
 change with 
 match true with
 [ true \Rightarrow False