changeset 35123 | e286d5df187a |
parent 35050 | 9f841f20dca6 |
child 35216 | 7641e8d831d2 |
--- a/src/HOL/Int.thy Sat Feb 13 23:16:06 2010 +0100 +++ b/src/HOL/Int.thy Sat Feb 13 23:24:57 2010 +0100 @@ -604,7 +604,7 @@ "_Numeral" :: "num_const \<Rightarrow> 'a" ("_") use "Tools/numeral_syntax.ML" -setup NumeralSyntax.setup +setup Numeral_Syntax.setup abbreviation "Numeral0 \<equiv> number_of Pls"