# HG changeset patch
# User paulson
# Date 931855351 -7200
# Node ID eed63543a3af3935b68f395bfe028e4483737749
# Parent  4e0defe58b4222214f3325351873ee927dddb8c8
renamed sort "numeral" to "number"

diff -r 4e0defe58b42 -r eed63543a3af src/HOL/Integ/Bin.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)"
diff -r 4e0defe58b42 -r eed63543a3af src/HOL/Numeral.thy
--- 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"	("_");