# HG changeset patch
# User haftmann
# Date 1331736867 -3600
# Node ID 53d06963d83d7d8a1d4b7479163fd3764bd120e0
# Parent  d2b92739038b3dbe09d8e955dba9afac8e98f300
corrected fragile proof; tuned semicolons

diff -r d2b92739038b -r 53d06963d83d doc-src/TutorialI/CTL/CTL.thy
--- 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)";