diff -r 23a8c5ac35f8 -r 69916a850301 doc-src/TutorialI/Overview/LNCS/Sets.thy
--- 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