# HG changeset patch
# User paulson
# Date 932743527 -7200
# Node ID a959b4391fd8abe0b2c8107ca7923efbdaf9d5eb
# Parent  c3f3fd86e11ccd300d35b162a5f055422c5d7480
added boolean and binary constants

diff -r c3f3fd86e11c -r a959b4391fd8 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Fri Jul 23 17:24:48 1999 +0200
+++ b/src/HOL/hologic.ML	Fri Jul 23 17:25:27 1999 +0200
@@ -11,6 +11,8 @@
   val termS: sort
   val termTVar: typ
   val boolT: typ
+  val false_const: term
+  val true_const: term
   val mk_setT: typ -> typ
   val dest_setT: typ -> typ
   val mk_Trueprop: term -> term
@@ -52,6 +54,11 @@
   val dest_Suc: term -> term
   val mk_nat: int -> term
   val dest_nat: term -> int
+  val intT: typ
+  val binT: typ
+  val pls_const: term
+  val min_const: term
+  val bit_const: term
 end;
 
 
@@ -70,11 +77,15 @@
 
 val boolT = Type ("bool", []);
 
+val true_const =  Const ("True", boolT)
+and false_const = Const ("False", boolT);
+
 fun mk_setT T = Type ("set", [T]);
 
 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);
 
@@ -205,4 +216,15 @@
   | dest_nat t = raise TERM ("dest_nat", [t]);
 
 
+val intT = Type ("IntDef.int", []);
+
+
+(* binary numerals *)
+
+val binT = Type ("Numeral.bin", []);
+
+val pls_const =  Const ("Numeral.bin.Pls", binT)
+and min_const = Const ("Numeral.bin.Min", binT)
+and bit_const = Const ("Numeral.bin.Bit", [binT, boolT] ---> binT);
+
 end;