--- a/src/HOL/Rational.thy Mon Feb 22 21:48:20 2010 -0800
+++ b/src/HOL/Rational.thy Tue Feb 23 07:45:54 2010 -0800
@@ -6,6 +6,7 @@
theory Rational
imports GCD Archimedean_Field
+uses ("Tools/float_syntax.ML")
begin
subsection {* Rational numbers as quotient *}
@@ -1212,4 +1213,15 @@
plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
zero_rat_inst.zero_rat
+subsection{* Float syntax *}
+
+syntax "_Float" :: "float_const \<Rightarrow> 'a" ("_")
+
+use "Tools/float_syntax.ML"
+setup Float_Syntax.setup
+
+text{* Test: *}
+lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
+by simp
+
end
--- a/src/HOL/RealPow.thy Mon Feb 22 21:48:20 2010 -0800
+++ b/src/HOL/RealPow.thy Tue Feb 23 07:45:54 2010 -0800
@@ -7,7 +7,6 @@
theory RealPow
imports RealDef
-uses ("Tools/float_syntax.ML")
begin
declare abs_mult_self [simp]
@@ -181,15 +180,4 @@
lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
by (case_tac "n", auto)
-subsection{* Float syntax *}
-
-syntax "_Float" :: "float_const \<Rightarrow> 'a" ("_")
-
-use "Tools/float_syntax.ML"
-setup Float_Syntax.setup
-
-text{* Test: *}
-lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::real)"
-by simp
-
end