]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/library/higher_order_defs/relations.ma
ocaml 3.09 transition
[helm.git] / helm / matita / library / higher_order_defs / relations.ma
index a2aa625a733e57491ad852b7f837374535291f25..029b229dc0f518edc78bca16ad317bd326ce59bb 100644 (file)
@@ -30,4 +30,4 @@ definition transitive: \forall A:Type.\forall R:A \to A \to Prop.Prop
 
 definition irreflexive: \forall A:Type.\forall R:A \to A \to Prop.Prop
 \def 
-\lambda A.\lambda R.\forall x:A.Not (R x x).
\ No newline at end of file
+\lambda A.\lambda R.\forall x:A.\lnot (R x x).