src/Doc/Tutorial/Rules/Forward.thy

--- a/src/Doc/Tutorial/Rules/Forward.thy	Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Rules/Forward.thy	Sat Nov 01 14:20:38 2014 +0100
@@ -11,7 +11,7 @@
 (** Commutativity **)
 
 lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
-apply (auto simp add: is_gcd_def);
+apply (auto simp add: is_gcd_def)
 done
 
 lemma gcd_commute: "gcd m n = gcd n m"
@@ -48,15 +48,15 @@
 text {*
 @{thm[display] gcd_mult_distrib2}
 \rulename{gcd_mult_distrib2}
-*};
+*}
 
 text{*\noindent
 of, simplified
 *}
 
 
-lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1];
-lemmas gcd_mult_1 = gcd_mult_0 [simplified];
+lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1]
+lemmas gcd_mult_1 = gcd_mult_0 [simplified]
 
 lemmas where1 = gcd_mult_distrib2 [where m=1]
 
@@ -82,23 +82,23 @@
 
 @{thm[display] sym}
 \rulename{sym}
-*};
+*}
 
-lemmas gcd_mult0 = gcd_mult_1 [THEN sym];
+lemmas gcd_mult0 = gcd_mult_1 [THEN sym]
       (*not quite right: we need ?k but this gives k*)
 
-lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym];
+lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym]
       (*better in one step!*)
 
 text {*
 more legible, and variables properly generalized
-*};
+*}
 
 lemma gcd_mult [simp]: "gcd k (k*n) = k"
 by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym])
 
 
-lemmas gcd_self0 = gcd_mult [of k 1, simplified];
+lemmas gcd_self0 = gcd_mult [of k 1, simplified]
 
 
 text {*
@@ -107,7 +107,7 @@
 
 @{thm[display] gcd_self0}
 \rulename{gcd_self0}
-*};
+*}
 
 text {*
 Rules handy with THEN
@@ -117,12 +117,12 @@
 
 @{thm[display] iffD2}
 \rulename{iffD2}
-*};
+*}
 
 
 text {*
 again: more legible, and variables properly generalized
-*};
+*}
 
 lemma gcd_self [simp]: "gcd k k = k"
 by (rule gcd_mult [of k 1, simplified])
@@ -143,12 +143,12 @@
 txt{*
 before using arg_cong
 @{subgoals[display,indent=0,margin=65]}
-*};
+*}
 apply (drule_tac f="\<lambda>x. x mod u" in arg_cong)
 txt{*
 after using arg_cong
 @{subgoals[display,indent=0,margin=65]}
-*};
+*}
 apply (simp add: mod_Suc)
 done
 
@@ -172,7 +172,7 @@
 txt{*@{subgoals[display,indent=0,margin=65]}*}
 apply simp
 txt{*@{subgoals[display,indent=0,margin=65]}*}
-apply (erule_tac t="m" in ssubst);
+apply (erule_tac t="m" in ssubst)
 apply simp
 done
 
@@ -185,16 +185,16 @@
 
 @{thm[display] mod_div_equality}
 \rulename{mod_div_equality}
-*};
+*}
 
 (*MOVED to Force.thy, which now depends only on Divides.thy
 lemma div_mult_self_is_m: "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
 *)
 
-lemma relprime_dvd_mult_iff: "gcd k n = 1 \<Longrightarrow> (k dvd m*n) = (k dvd m)";
+lemma relprime_dvd_mult_iff: "gcd k n = 1 \<Longrightarrow> (k dvd m*n) = (k dvd m)"
 by (auto intro: relprime_dvd_mult elim: dvdE)
 
-lemma relprime_20_81: "gcd 20 81 = 1";
+lemma relprime_20_81: "gcd 20 81 = 1"
 by (simp add: gcd.simps)
 
 text {*
@@ -214,20 +214,20 @@
 @{thm[display] dvd_add [OF dvd_refl dvd_refl]}
 
 @{thm[display] dvd_add [OF _ dvd_refl]}
-*};
+*}
 
-lemma "\<lbrakk>(z::int) < 37; 66 < 2*z; z*z \<noteq> 1225; Q(34); Q(36)\<rbrakk> \<Longrightarrow> Q(z)";
+lemma "\<lbrakk>(z::int) < 37; 66 < 2*z; z*z \<noteq> 1225; Q(34); Q(36)\<rbrakk> \<Longrightarrow> Q(z)"
 apply (subgoal_tac "z = 34 \<or> z = 36")
 txt{*
 the tactic leaves two subgoals:
 @{subgoals[display,indent=0,margin=65]}
-*};
+*}
 apply blast
 apply (subgoal_tac "z \<noteq> 35")
 txt{*
 the tactic leaves two subgoals:
 @{subgoals[display,indent=0,margin=65]}
-*};
+*}
 apply arith
 apply force
 done