Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nonstandard_Analysis/HLim.thy
changeset 64604 2bf8cfc98c4d
parent 64435 c93b0e6131c3
child 66827 c94531b5007d 
--- a/src/HOL/Nonstandard_Analysis/HLim.thy	Sun Dec 18 22:14:53 2016 +0100
+++ b/src/HOL/Nonstandard_Analysis/HLim.thy	Sun Dec 18 23:43:50 2016 +0100
@@ -77,7 +77,7 @@
 qed
 
 lemma NSLIM_zero_cancel: "(\<lambda>x. f x - l) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0 \<Longrightarrow> f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l"
-  apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
+  apply (drule_tac g = "\<lambda>x. l" and m = l in NSLIM_add)
    apply (auto simp add: add.assoc)
   done
 
@@ -205,8 +205,8 @@
 lemma isCont_isNSCont: "isCont f a \<Longrightarrow> isNSCont f a"
   by (erule isNSCont_isCont_iff [THEN iffD2])
 
-text \<open>NS continuity \<open>==>\<close> Standard continuity.\<close>
-lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
+text \<open>NS continuity \<open>\<Longrightarrow>\<close> Standard continuity.\<close>
+lemma isNSCont_isCont: "isNSCont f a \<Longrightarrow> isCont f a"
   by (erule isNSCont_isCont_iff [THEN iffD1])
isabelle