# HG changeset patch
# User wenzelm
# Date 952949872 -3600
# Node ID 515fa75333542a810efe6041d12d4905b3d43089
# Parent  be4c8a57cf7e8b1f1c5a9aa7f6d7f48a63e3ccf2
added Not;

diff -r be4c8a57cf7e -r 515fa7533354 src/HOL/hologic.ML
--- 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