src/HOL/RealPow.thy
changeset 35123 e286d5df187a
parent 31021 53642251a04f
child 35216 7641e8d831d2
     1.1 --- a/src/HOL/RealPow.thy	Sat Feb 13 23:16:06 2010 +0100
     1.2 +++ b/src/HOL/RealPow.thy	Sat Feb 13 23:24:57 2010 +0100
     1.3 @@ -186,7 +186,7 @@
     1.4  syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
     1.5  
     1.6  use "Tools/float_syntax.ML"
     1.7 -setup FloatSyntax.setup
     1.8 +setup Float_Syntax.setup
     1.9  
    1.10  text{* Test: *}
    1.11  lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::real)"