--- a/doc-src/TutorialI/CTL/CTL.thy Wed Mar 14 15:24:51 2012 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy Wed Mar 14 15:54:27 2012 +0100
@@ -370,11 +370,11 @@
lemma "lfp(eufix A B) \<subseteq> eusem A B"
apply(rule lfp_lowerbound)
-apply(auto simp add: eusem_def eufix_def);
- apply(rule_tac x = "[]" in exI);
+apply(auto simp add: eusem_def eufix_def)
+ apply(rule_tac x = "[]" in exI)
apply simp
-apply(rule_tac x = "y#xc" in exI);
-apply simp;
+apply(rule_tac x = "xa#xb" in exI)
+apply simp
done
lemma mono_eufix: "mono(eufix A B)";