# HG changeset patch
# User wenzelm
# Date 1121362097 -7200
# Node ID 2e7d7ec7a268d4bf049758c9a83cf41b116f9f55
# Parent  71d87aeebb5730f75fd8f2cc810ca791d9069a4a
removed not_const -- use Not instead;
add mk_not;

diff -r 71d87aeebb57 -r 2e7d7ec7a268 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Thu Jul 14 19:28:16 2005 +0200
+++ b/src/HOL/hologic.ML	Thu Jul 14 19:28:17 2005 +0200
@@ -14,7 +14,6 @@
   val boolT: typ
   val false_const: term
   val true_const: term
-  val not_const: term
   val mk_setT: typ -> typ
   val dest_setT: typ -> typ
   val Trueprop: term
@@ -27,6 +26,7 @@
   val mk_conj: term * term -> term
   val mk_disj: term * term -> term
   val mk_imp: term * term -> term
+  val mk_not: term -> term
   val dest_conj: term -> term list
   val dest_disj: term -> term list
   val dest_imp: term -> term * term
@@ -108,7 +108,6 @@
 
 val true_const =  Const ("True", boolT);
 val false_const = Const ("False", boolT);
-val not_const = Const ("Not", boolT --> boolT);
 
 fun mk_setT T = Type ("set", [T]);
 
@@ -133,7 +132,8 @@
 
 fun mk_conj (t1, t2) = conj $ t1 $ t2
 and mk_disj (t1, t2) = disj $ t1 $ t2
-and mk_imp (t1, t2) = imp $ t1 $ t2;
+and mk_imp (t1, t2) = imp $ t1 $ t2
+and mk_not t = Not $ t;
 
 fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
   | dest_conj t = [t];