Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/FOL/fologic.ML
changeset 9850 bee6eb4b6a42
parent 9543 ce61d1c1a509
child 10384 a499b9ce2ffe 
--- a/src/FOL/fologic.ML	Tue Sep 05 18:45:09 2000 +0200
+++ b/src/FOL/fologic.ML	Tue Sep 05 18:45:51 2000 +0200
@@ -11,6 +11,7 @@
   val mk_Trueprop	: term -> term
   val atomic_Trueprop	: string -> term
   val dest_Trueprop	: term -> term
+  val not		: term
   val conj		: term
   val disj		: term
   val imp		: term
@@ -50,10 +51,11 @@
 
 (** Logical constants **)
 
-val conj = Const("op &", [oT,oT]--->oT)
-and disj = Const("op |", [oT,oT]--->oT)
-and imp = Const("op -->", [oT,oT]--->oT)
-and iff = Const("op <->", [oT,oT]--->oT);
+val not = Const ("Not", oT --> oT);
+val conj = Const("op &", [oT,oT]--->oT);
+val disj = Const("op |", [oT,oT]--->oT);
+val imp = Const("op -->", [oT,oT]--->oT)
+val iff = Const("op <->", [oT,oT]--->oT);
 
 fun mk_conj (t1, t2) = conj $ t1 $ t2
 and mk_disj (t1, t2) = disj $ t1 $ t2
isabelle