diff -r c57ec95e7763 -r ca5029d391d1 doc-src/TutorialI/Overview/LNCS/Sets.thy
--- a/doc-src/TutorialI/Overview/LNCS/Sets.thy	Thu Jul 31 00:01:47 2003 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/Sets.thy	Thu Jul 31 14:01:04 2003 +0200
@@ -39,15 +39,12 @@
 @{thm converse_def[no_vars]}\\
 @{thm Image_def[no_vars]}\\
 @{thm rtrancl_refl[no_vars]}\\
-@{thm rtrancl_into_rtrancl[no_vars]}\\
-@{thm trancl_def[no_vars]}
+@{thm rtrancl_into_rtrancl[no_vars]}
 \end{tabular}*}
 (*<*)thm Id_def
-thm converse_def[no_vars]
-thm Image_def[no_vars]
+thm converse_def[no_vars] Image_def[no_vars]
 thm relpow.simps[no_vars]
-thm rtrancl.intros[no_vars]
-thm trancl_def[no_vars](*>*)
+thm rtrancl.intros[no_vars](*>*)
 
 
 subsection{*Wellfoundedness*}
@@ -69,9 +66,9 @@
 @{thm lfp_unfold[no_vars]}\\
 @{thm lfp_induct[no_vars]}
 \end{tabular}*}
-(*<*)thm lfp_def gfp_def
-thm lfp_unfold
-thm lfp_induct(*>*)
+(*<*)thm lfp_def[no_vars] gfp_def[no_vars]
+thm lfp_unfold[no_vars]
+thm lfp_induct[no_vars](*>*)
 
 
 subsection{*Case Study: Verified Model Checking*}
@@ -133,6 +130,39 @@
 apply(auto simp add: EF_lemma)
 done
 
+text{*Preview of coming attractions: a structured proof of the
+@{thm[source]EF_lemma}.*}
+lemma EF_lemma:
+  "lfp(\<lambda>T. A \<union> (M\<inverse> `` T)) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"
+  (is "lfp ?F = ?R") 
+proof
+  show "lfp ?F \<subseteq> ?R"
+  proof (rule lfp_lowerbound)
+    show "?F ?R \<subseteq> ?R" by(blast intro: rtrancl_trans)
+  qed
+next
+  show "?R \<subseteq> lfp ?F"
+  proof
+    fix s assume "s \<in> ?R"
+    then obtain t where st: "(s,t) \<in> M\<^sup>*" and tA: "t \<in> A" by blast
+    from st show "s \<in> lfp ?F"
+    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
+      qed
+    next
+      fix s s'
+      assume ss': "(s,s') \<in> M" and s't: "(s',t) \<in> M\<^sup>*"
+         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
+      qed
+    qed
+  qed
+qed
+
 text{*
 \begin{exercise}
 @{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX}