--- a/ProgTutorial/Tactical.thy	Tue May 21 16:22:30 2019 +0200
+++ b/ProgTutorial/Tactical.thy	Wed May 22 12:38:51 2019 +0200
@@ -962,7 +962,8 @@
 lemma 
   shows "A \<Longrightarrow> True \<and> A"
 apply(tactic \<open>(resolve_tac @{context} [@{thm conjI}] 
-                 THEN' RANGE [resolve_tac @{context} [@{thm TrueI}], assume_tac @{context}]) 1\<close>)
+               THEN' RANGE [resolve_tac @{context} [@{thm TrueI}], 
+                            assume_tac @{context}]) 1\<close>)
 txt \<open>\begin{minipage}{\textwidth}
        @{subgoals [display]} 
        \end{minipage}\<close>
@@ -976,8 +977,11 @@
 \<close>
 
 ML %grayML\<open>fun foo_tac'' ctxt = 
-  EVERY' [eresolve_tac ctxt [@{thm disjE}], resolve_tac ctxt [@{thm disjI2}], 
-          assume_tac ctxt, resolve_tac ctxt [@{thm disjI1}], assume_tac ctxt]\<close>
+  EVERY' [eresolve_tac ctxt [@{thm disjE}], 
+          resolve_tac ctxt [@{thm disjI2}], 
+          assume_tac ctxt, 
+          resolve_tac ctxt [@{thm disjI1}], 
+          assume_tac ctxt]\<close>
 
 text \<open>
   There is even another way of implementing this tactic: in automatic proof
@@ -988,8 +992,11 @@
 \<close>
 
 ML %grayML\<open>fun foo_tac1 ctxt = 
-  EVERY1 [eresolve_tac ctxt [@{thm disjE}], resolve_tac ctxt [@{thm disjI2}], 
-          assume_tac ctxt, resolve_tac ctxt [@{thm disjI1}], assume_tac ctxt]\<close>
+  EVERY1 [eresolve_tac ctxt [@{thm disjE}], 
+          resolve_tac ctxt [@{thm disjI2}], 
+          assume_tac ctxt, 
+          resolve_tac ctxt [@{thm disjI1}], 
+          assume_tac ctxt]\<close>
 
 text \<open>
   and call @{ML foo_tac1}.  
@@ -1073,8 +1080,10 @@
 \<close>
 
 ML %grayML\<open>fun select_tac'' ctxt = 
- TRY o FIRST' [resolve_tac ctxt [@{thm conjI}], resolve_tac ctxt [@{thm impI}], 
-               resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}]]\<close>
+ TRY o FIRST' [resolve_tac ctxt [@{thm conjI}], 
+               resolve_tac ctxt [@{thm impI}], 
+               resolve_tac ctxt [@{thm notI}], 
+               resolve_tac ctxt [@{thm allI}]]\<close>
 text_raw\<open>\label{tac:selectprimeprime}\<close>
 
 text \<open>
@@ -1472,7 +1481,8 @@
   the simplification rule @{thm [source] Diff_Int} as follows:
 \<close>
 
-ML %grayML\<open>val ss1 = put_simpset empty_ss @{context} addsimps [@{thm Diff_Int} RS @{thm eq_reflection}]\<close>
+ML %grayML\<open>val ss1 = put_simpset empty_ss @{context} addsimps 
+  [@{thm Diff_Int} RS @{thm eq_reflection}]\<close>
 
 thm "INF_cong"
 text \<open>
@@ -1490,7 +1500,8 @@
   Adding also the congruence rule @{thm [source] INF_cong} 
 \<close>
 
-ML %grayML\<open>val ss2 = ss1 |> Simplifier.add_cong (@{thm INF_cong} RS @{thm eq_reflection})\<close>
+ML %grayML\<open>val ss2 = ss1 |> 
+  Simplifier.add_cong (@{thm INF_cong} RS @{thm eq_reflection})\<close>
 
 text \<open>
   gives
@@ -1501,7 +1512,8 @@
   ??.unknown: A1 - B1 \<inter> C1 \<equiv> A1 - B1 \<union> (A1 - C1)
 Congruences rules:
   Complete_Lattices.Inf_class.Inf: 
-    \<lbrakk>A1 = B1; \<And>x. x \<in> B1 \<Longrightarrow> C1 x = D1 x\<rbrakk> \<Longrightarrow> Inf (C1 ` A1) \<equiv> Inf (D1 ` B1)
+    \<lbrakk>A1 = B1; \<And>x. x \<in> B1 \<Longrightarrow> C1 x = D1 x\<rbrakk> 
+    \<Longrightarrow> Inf (C1 ` A1) \<equiv> Inf (D1 ` B1)
 Simproc patterns:\<close>}
 
   Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss}