# 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 \ '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 \ '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