changeset 12338 | de0f4a63baa5 |
parent 12098 | 784fe681ba26 |
child 12738 | 9d80e3746eb0 |
--- a/src/HOL/Numeral.thy Sat Dec 01 18:51:46 2001 +0100 +++ b/src/HOL/Numeral.thy Sat Dec 01 18:52:32 2001 +0100 @@ -14,7 +14,7 @@ | Bit bin bool (infixl "BIT" 90) axclass - number < "term" (*for numeric types: nat, int, real, ...*) + number < type -- {* for numeric types: nat, int, real, \dots *} consts number_of :: "bin => 'a::number"