1.1 --- a/src/HOL/Library/Extended_Real.thy	Wed Jul 20 15:09:53 2011 +0200
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Jul 20 15:42:23 2011 +0200
     1.3 @@ -75,6 +75,15 @@
     1.4      and MInfty_cases[simp]: "(case - \<infinity> of ereal r \<Rightarrow> f r | PInfty \<Rightarrow> y | MInfty \<Rightarrow> z) = z"
     1.5    by (simp_all add: infinity_ereal_def)
     1.6  
     1.7 +declare
     1.8 +  PInfty_eq_infinity[code_post]
     1.9 +  MInfty_eq_minfinity[code_post]
    1.10 +
    1.11 +lemma [code_unfold]:
    1.12 +  "\<infinity> = PInfty"
    1.13 +  "-PInfty = MInfty"
    1.14 +  by simp_all
    1.15 +
    1.16  lemma inj_ereal[simp]: "inj_on ereal A"
    1.17    unfolding inj_on_def by auto
    1.18  
    1.19 @@ -2540,4 +2549,14 @@
    1.20    "[| (a::ereal) <= x; c <= x |] ==> max a c <= x"
    1.21    by (metis sup_ereal_def sup_least)
    1.22  
    1.23 +subsubsection {* Tests for code generator *}
    1.24 +
    1.25 +(* A small list of simple arithmetic expressions *)
    1.26 +
    1.27 +value [code] "- \<infinity> :: ereal"
    1.28 +value [code] "\<bar>-\<infinity>\<bar> :: ereal"
    1.29 +value [code] "4 + 5 / 4 - ereal 2 :: ereal"
    1.30 +value [code] "ereal 3 < \<infinity>"
    1.31 +value [code] "real (\<infinity>::ereal) = 0"
    1.32 +
    1.33  end