# HG changeset patch
# User wenzelm
# Date 968172502 -7200
# Node ID c34d3c94298c9c51e40144d855baa05e7c15929b
# Parent  709a295731e2b18443be17ff39af2da4cd995915
added not_const;

diff -r 709a295731e2 -r c34d3c94298c src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Tue Sep 05 18:48:04 2000 +0200
+++ b/src/HOL/hologic.ML	Tue Sep 05 18:48:22 2000 +0200
@@ -14,6 +14,7 @@
   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 mk_Trueprop: term -> term
@@ -89,8 +90,9 @@
 val boolN = "bool";
 val boolT = Type (boolN, []);
 
-val true_const =  Const ("True", boolT)
-and false_const = Const ("False", boolT);
+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]);