src/HOL/Numeral.thy
changeset 6988 eed63543a3af
parent 6905 9bc05ec3497b
child 9035 371f023d3dbd
     1.1 --- a/src/HOL/Numeral.thy	Tue Jul 13 10:41:59 1999 +0200
     1.2 +++ b/src/HOL/Numeral.thy	Tue Jul 13 10:42:31 1999 +0200
     1.3 @@ -14,10 +14,10 @@
     1.4        | Bit bin bool	(infixl "BIT" 90);
     1.5  
     1.6  axclass
     1.7 -  numeral < "term";
     1.8 +  number < "term";      (*for numeric types: nat, int, real, ...*)
     1.9  
    1.10  consts
    1.11 -  number_of :: "bin => 'a::numeral";
    1.12 +  number_of :: "bin => 'a::number";
    1.13  
    1.14  syntax
    1.15    "_Numeral" :: "xnum => 'a"	("_");