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.
doc-src/TutorialI/Overview/LNCS/Sets.thy
changeset 32960 69916a850301
parent 21324 a5089fc012b5 
--- a/doc-src/TutorialI/Overview/LNCS/Sets.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/Sets.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -149,7 +149,7 @@
     proof (rule converse_rtrancl_induct)
       show "t \<in> lfp ?F"
       proof (subst lfp_unfold[OF mono_ef])
-	show "t \<in> ?F(lfp ?F)" using tA by blast
+        show "t \<in> ?F(lfp ?F)" using tA by blast
       qed
     next
       fix s s'
@@ -157,7 +157,7 @@
          and IH: "s' \<in> lfp ?F"
       show "s \<in> lfp ?F"
       proof (subst lfp_unfold[OF mono_ef])
-	show "s \<in> ?F(lfp ?F)" using prems by blast
+        show "s \<in> ?F(lfp ?F)" using prems by blast
       qed
     qed
   qed
isabelle