More notation here and there.

[helm.git] / helm / matita / library / datatypes / bool.ma

diff --git a/helm/matita/library/datatypes/bool.ma b/helm/matita/library/datatypes/bool.ma
index d99456dc89e1b02ee4522c26ee90cc5ab6930ded..a223d7d0c9333c27b77e328b253e19229fe319f1 100644 (file)
--- 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