--- a/src/HOL/Tools/Presburger/presburger.ML Wed Mar 23 12:08:52 2005 +0100
+++ b/src/HOL/Tools/Presburger/presburger.ML Wed Mar 23 12:09:18 2005 +0100
@@ -75,6 +75,7 @@
(* SOME Types*)
val bT = HOLogic.boolT;
+val bitT = HOLogic.bitT;
val iT = HOLogic.intT;
val binT = HOLogic.binT;
val nT = HOLogic.natT;
@@ -120,7 +121,9 @@
("HOL.max", nT --> nT --> nT),
("HOL.min", nT --> nT --> nT),
- ("Numeral.Bit", binT --> bT --> binT),
+ ("Numeral.bit.B0", bitT),
+ ("Numeral.bit.B1", bitT),
+ ("Numeral.Bit", binT --> bitT --> binT),
("Numeral.Pls", binT),
("Numeral.Min", binT),
("Numeral.number_of", binT --> iT),