--- a/src/HOL/hologic.ML Mon Mar 13 13:16:57 2000 +0100
+++ b/src/HOL/hologic.ML Mon Mar 13 13:17:52 2000 +0100
@@ -21,6 +21,7 @@
val conj: term
val disj: term
val imp: term
+ val Not: term
val mk_conj: term * term -> term
val mk_disj: term * term -> term
val mk_imp: term * term -> term
@@ -106,7 +107,8 @@
val conj = Const ("op &", [boolT, boolT] ---> boolT)
and disj = Const ("op |", [boolT, boolT] ---> boolT)
-and imp = Const ("op -->", [boolT, boolT] ---> boolT);
+and imp = Const ("op -->", [boolT, boolT] ---> boolT)
+and Not = Const ("Not", boolT --> boolT);
fun mk_conj (t1, t2) = conj $ t1 $ t2
and mk_disj (t1, t2) = disj $ t1 $ t2