src/HOL/Real/RealPow.thy
changeset 28906 5f568bfc58d7
parent 26565 522f45a8604e
     1.1 --- a/src/HOL/Real/RealPow.thy	Sat Nov 29 13:39:23 2008 +0100
     1.2 +++ b/src/HOL/Real/RealPow.thy	Sat Nov 29 13:39:45 2008 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  
     1.5  theory RealPow
     1.6  imports RealDef
     1.7 +uses ("float_syntax.ML")
     1.8  begin
     1.9  
    1.10  declare abs_mult_self [simp]
    1.11 @@ -267,4 +268,15 @@
    1.12  lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
    1.13  by (case_tac "n", auto)
    1.14  
    1.15 +subsection{* Float syntax *}
    1.16 +
    1.17 +syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
    1.18 +
    1.19 +use "float_syntax.ML"
    1.20 +setup FloatSyntax.setup
    1.21 +
    1.22 +text{* Test: *}
    1.23 +lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::real)"
    1.24 +by simp
    1.25 +
    1.26  end