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/Hyperreal/SEQ.thy
changeset 28823 dcbef866c9e2
parent 28562 4e74209f113e
child 28944 e27abf0db984 
--- a/src/HOL/Hyperreal/SEQ.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Hyperreal/SEQ.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -935,7 +935,7 @@
 lemma real_CauchyI:
   assumes "Cauchy X"
   shows "real_Cauchy X"
-by unfold_locales (fact assms)
+  proof qed (fact assms)
 
 lemma (in real_Cauchy) mem_S: "\<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S"
 by (unfold S_def, auto)
isabelle