--- a/src/HOL/hologic.ML Tue Apr 18 15:54:31 2000 +0200
+++ b/src/HOL/hologic.ML Tue Apr 18 15:54:56 2000 +0200
@@ -66,6 +66,7 @@
val pls_const: term
val min_const: term
val bit_const: term
+ val number_of_const: term
val int_of: int list -> int
val dest_binum: term -> int
end;
@@ -245,7 +246,9 @@
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);
+and bit_const = Const ("Numeral.bin.Bit", [binT, boolT] ---> binT)
+and number_of_const = Const ("Numeral.number_of", binT --> natT);
+
fun int_of [] = 0
| int_of (b :: bs) = b + 2 * int_of bs;