# HG changeset patch
# User huffman
# Date 1266939954 28800
# Node ID 523124691b3a08d1fd5a862a67d1fc00e4303410
# Parent  0e1adc24722ff841595206ce59e0b4d517a73819
move float syntax from RealPow to Rational

diff -r 0e1adc24722f -r 523124691b3a src/HOL/Rational.thy
--- 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
diff -r 0e1adc24722f -r 523124691b3a src/HOL/RealPow.thy
--- 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