renamed sort "numeral" to "number"
authorpaulson
Tue, 13 Jul 1999 10:42:31 +0200
changeset 6988 eed63543a3af
parent 6987 4e0defe58b42
child 6989 dd3e8bd86cc6
renamed sort "numeral" to "number"
src/HOL/Integ/Bin.thy
src/HOL/Numeral.thy
--- 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"	("_");