X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fdatatypes%2Fbool.ma;h=f4aec8167476b0d88204a06d3d23aaa798a323ac;hb=400b07e007cfbb0b4ce5ed77cfc50f227c491310;hp=11f1d7a8c49d48047e12caaeec555c207e1ca784;hpb=5538a4548601ba1c1647ec9dc0fbbd875e5a93fd;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