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