src/ZF/Bin.thy
changeset 35123 e286d5df187a
parent 35112 ff6f60e6ab85
child 45703 c7a13ce60161
     1.1 --- a/src/ZF/Bin.thy	Sat Feb 13 23:16:06 2010 +0100
     1.2 +++ b/src/ZF/Bin.thy	Sat Feb 13 23:24:57 2010 +0100
     1.3 @@ -105,7 +105,7 @@
     1.4    "_Int"    :: "xnum => i"        ("_")
     1.5  
     1.6  use "Tools/numeral_syntax.ML"
     1.7 -setup NumeralSyntax.setup
     1.8 +setup Numeral_Syntax.setup
     1.9  
    1.10  
    1.11  declare bin.intros [simp,TC]