--- a/src/HOL/Integ/Bin.thy Tue Jul 13 10:41:59 1999 +0200
+++ b/src/HOL/Integ/Bin.thy Tue Jul 13 10:42:31 1999 +0200
@@ -40,7 +40,8 @@
NCons_BIT "NCons (w BIT x) b = (w BIT x) BIT b"
instance
- int :: numeral
+ int :: number
+
primrec
number_of_Pls "number_of Pls = int 0"
number_of_Min "number_of Min = - (int 1)"
--- a/src/HOL/Numeral.thy Tue Jul 13 10:41:59 1999 +0200
+++ b/src/HOL/Numeral.thy Tue Jul 13 10:42:31 1999 +0200
@@ -14,10 +14,10 @@
| Bit bin bool (infixl "BIT" 90);
axclass
- numeral < "term";
+ number < "term"; (*for numeric types: nat, int, real, ...*)
consts
- number_of :: "bin => 'a::numeral";
+ number_of :: "bin => 'a::number";
syntax
"_Numeral" :: "xnum => 'a" ("_");