src/HOL/Analysis/Linear_Algebra.thy
changeset 67443 3abf6a722518
parent 67399 eab6ce8368fa
child 67685 bdff8bf0a75b
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Jan 16 09:12:16 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Tue Jan 16 09:30:00 2018 +0100
     1.3 @@ -1726,7 +1726,7 @@
     1.4    apply auto
     1.5    done
     1.6  
     1.7 -lemma approachable_lt_le2:  \<comment>\<open>like the above, but pushes aside an extra formula\<close>
     1.8 +lemma approachable_lt_le2:  \<comment> \<open>like the above, but pushes aside an extra formula\<close>
     1.9      "(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
    1.10    apply auto
    1.11    apply (rule_tac x="d/2" in exI, auto)