src/Doc/Tutorial/Inductive/Star.thy
changeset 58860 fee7cfa69c50
parent 48985 5386df44a037
child 67406 23307fd33906
--- a/src/Doc/Tutorial/Inductive/Star.thy	Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Inductive/Star.thy	Sat Nov 01 14:20:38 2014 +0100
@@ -39,7 +39,7 @@
 *}
 
 lemma [intro]: "(x,y) \<in> r \<Longrightarrow> (x,y) \<in> r*"
-by(blast intro: rtc_step);
+by(blast intro: rtc_step)
 
 text{*\noindent
 Although the lemma itself is an unremarkable consequence of the basic rules,
@@ -110,8 +110,8 @@
 @{subgoals[display,indent=0]}
 *}
 
- apply(blast);
-apply(blast intro: rtc_step);
+ apply(blast)
+apply(blast intro: rtc_step)
 done
 
 text{*
@@ -134,16 +134,16 @@
 *}
 
 lemma "(x,y) \<in> rtc2 r \<Longrightarrow> (x,y) \<in> r*"
-apply(erule rtc2.induct);
-  apply(blast);
- apply(blast);
-apply(blast intro: rtc_trans);
+apply(erule rtc2.induct)
+  apply(blast)
+ apply(blast)
+apply(blast intro: rtc_trans)
 done
 
 lemma "(x,y) \<in> r* \<Longrightarrow> (x,y) \<in> rtc2 r"
-apply(erule rtc.induct);
- apply(blast intro: rtc2.intros);
-apply(blast intro: rtc2.intros);
+apply(erule rtc.induct)
+ apply(blast intro: rtc2.intros)
+apply(blast intro: rtc2.intros)
 done
 
 text{*
@@ -167,8 +167,8 @@
 *}
 (*<*)
 lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r --> (x,z) : r*"
-apply(erule rtc.induct);
- apply blast;
+apply(erule rtc.induct)
+ apply blast
 apply(blast intro: rtc_step)
 done