X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fdatatypes%2Fbool.ma;h=a223d7d0c9333c27b77e328b253e19229fe319f1;hb=2c22c8fe144cbce796168ffd9843a87f06dcfa76;hp=d99456dc89e1b02ee4522c26ee90cc5ab6930ded;hpb=03fcee16d9c262aad38a47d0a409b684a965cc3f;p=helm.git

diff --git a/helm/matita/library/datatypes/bool.ma b/helm/matita/library/datatypes/bool.ma
index d99456dc8..a223d7d0c 100644
--- a/helm/matita/library/datatypes/bool.ma
+++ b/helm/matita/library/datatypes/bool.ma
@@ -20,7 +20,7 @@ inductive bool : Set \def
   | true : bool
   | false : bool.
   
-theorem not_eq_true_false : \lnot true = false.
+theorem not_eq_true_false : true \neq false.
 simplify.intro.
 change with 
 match true with