renamed sort "numeral" to "number"
authorpaulson
Tue Jul 13 10:42:31 1999 +0200 (1999-07-13)
changeset 6988eed63543a3af
parent 6987 4e0defe58b42
child 6989 dd3e8bd86cc6
renamed sort "numeral" to "number"
src/HOL/Integ/Bin.thy
src/HOL/Numeral.thy
     1.1 --- a/src/HOL/Integ/Bin.thy	Tue Jul 13 10:41:59 1999 +0200
     1.2 +++ b/src/HOL/Integ/Bin.thy	Tue Jul 13 10:42:31 1999 +0200
     1.3 @@ -40,7 +40,8 @@
     1.4    NCons_BIT "NCons (w BIT x) b = (w BIT x) BIT b"
     1.5  
     1.6  instance
     1.7 -  int :: numeral 
     1.8 +  int :: number
     1.9 +
    1.10  primrec
    1.11    number_of_Pls  "number_of Pls = int 0"
    1.12    number_of_Min  "number_of Min = - (int 1)"
     2.1 --- a/src/HOL/Numeral.thy	Tue Jul 13 10:41:59 1999 +0200
     2.2 +++ b/src/HOL/Numeral.thy	Tue Jul 13 10:42:31 1999 +0200
     2.3 @@ -14,10 +14,10 @@
     2.4        | Bit bin bool	(infixl "BIT" 90);
     2.5  
     2.6  axclass
     2.7 -  numeral < "term";
     2.8 +  number < "term";      (*for numeric types: nat, int, real, ...*)
     2.9  
    2.10  consts
    2.11 -  number_of :: "bin => 'a::numeral";
    2.12 +  number_of :: "bin => 'a::number";
    2.13  
    2.14  syntax
    2.15    "_Numeral" :: "xnum => 'a"	("_");