equal
deleted
inserted
replaced
57 |
57 |
58 definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)" |
58 definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)" |
59 |
59 |
60 declare [[coercion "ereal :: real \<Rightarrow> ereal"]] |
60 declare [[coercion "ereal :: real \<Rightarrow> ereal"]] |
61 declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]] |
61 declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]] |
62 declare [[coercion "(\<lambda>n. ereal (of_nat n)) :: nat \<Rightarrow> ereal"]] |
62 declare [[coercion "(\<lambda>n. ereal (real n)) :: nat \<Rightarrow> ereal"]] |
63 |
63 |
64 lemma ereal_uminus_uminus[simp]: |
64 lemma ereal_uminus_uminus[simp]: |
65 fixes a :: ereal shows "- (- a) = a" |
65 fixes a :: ereal shows "- (- a) = a" |
66 by (cases a) simp_all |
66 by (cases a) simp_all |
67 |
67 |