# HG changeset patch
# User wenzelm
# Date 968172351 -7200
# Node ID bee6eb4b6a42659d76ac7d1e93795cb263fae06f
# Parent  71ad08ad2cf02c43441a554af989df930ec7d14c
added not;

diff -r 71ad08ad2cf0 -r bee6eb4b6a42 src/FOL/fologic.ML
--- 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