# HG changeset patch
# User paulson
# Date 956066096 -7200
# Node ID 60a1ed9e3c343b5eaef6ecb1b9db1369bc1ab3ac
# Parent  e583d8987abb91123481d7f13288b2c03657a5cb
added number_of_const: term

diff -r e583d8987abb -r 60a1ed9e3c34 src/HOL/hologic.ML
--- 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;