A little bit more of notation here and there.

[helm.git] / helm / matita / library / Z / z.ma

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index 5aa5d90832a7359dc9da1d20d6581c1e1a3b7a21..9dffcee52c9098e6d4488b443d8ba79f4b5958ec 100644 (file)
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -52,7 +52,7 @@ match z with
 theorem OZ_test_to_Prop :\forall z:Z.
 match OZ_test z with
 [true \Rightarrow eq Z z OZ 
-|false \Rightarrow Not (eq Z z OZ)].
+|false \Rightarrow \lnot (eq Z z OZ)].
 intros.elim z.
 simplify.reflexivity.
 simplify.intros.