--- a/src/HOL/hologic.ML Tue Feb 22 20:16:07 2000 +0100
+++ b/src/HOL/hologic.ML Tue Feb 22 21:39:01 2000 +0100
@@ -10,6 +10,7 @@
val termC: class
val termS: sort
val termT: typ
+ val boolN: string
val boolT: typ
val false_const: term
val true_const: term
@@ -80,7 +81,8 @@
(* bool and set *)
-val boolT = Type ("bool", []);
+val boolN = "bool";
+val boolT = Type (boolN, []);
val true_const = Const ("True", boolT)
and false_const = Const ("False", boolT);
@@ -90,6 +92,7 @@
fun dest_setT (Type ("set", [T])) = T
| dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
+
(* logic *)
val Trueprop = Const ("Trueprop", boolT --> propT);