changeset 12098 | 784fe681ba26 |
parent 11868 | 56db9f3a6b3e |
child 12338 | de0f4a63baa5 |
--- a/src/HOL/Numeral.thy Thu Nov 08 00:25:09 2001 +0100 +++ b/src/HOL/Numeral.thy Thu Nov 08 00:25:36 2001 +0100 @@ -19,12 +19,8 @@ consts number_of :: "bin => 'a::number" -nonterminals - numeral - syntax - "_constify" :: "num => numeral" ("_") - "_Numeral" :: "numeral => 'a" ("_") + "_Numeral" :: "num_const => 'a" ("_") Numeral0 :: 'a Numeral1 :: 'a