| changeset 65578 | e4997c181cce |
| parent 65036 | ab7e11730ad8 |
| child 65583 | 8d53b3bebab4 |
--- a/src/HOL/Real_Vector_Spaces.thy Tue Apr 25 08:38:23 2017 +0200 +++ b/src/HOL/Real_Vector_Spaces.thy Tue Apr 25 16:39:54 2017 +0100 @@ -364,6 +364,7 @@ by (auto intro: injI) lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified] +lemmas of_real_eq_1_iff [simp] = of_real_eq_iff [of _ 1, simplified] lemma of_real_eq_id [simp]: "of_real = (id :: real \<Rightarrow> real)" by (rule ext) (simp add: of_real_def)