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