--- a/ProgTutorial/Tactical.thy	Wed May 22 12:38:51 2019 +0200
+++ b/ProgTutorial/Tactical.thy	Wed May 22 13:24:30 2019 +0200
@@ -1724,9 +1724,9 @@
   after one step. In this way, we can split simplification of permutations
   into three phases without the user noticing anything about the auxiliary 
   constant. We first freeze any instance of permutation compositions in the term using 
-  lemma @{thm [source] "perm_aux_expand"} (Line 9);
+  lemma @{thm [source] "perm_aux_expand"} (Line 10);
   then simplify all other permutations including pushing permutations over
-  other permutations by rule @{thm [source] perm_compose_aux} (Line 10); and
+  other permutations by rule @{thm [source] perm_compose_aux} (Line 11); and
   finally ``unfreeze'' all instances of permutation compositions by unfolding 
   the definition of the auxiliary constant. 
 \<close>
@@ -1800,8 +1800,7 @@
 
 text \<open>
   This function takes a simpset and a redex (a @{ML_type cterm}) as
-  arguments. In Lines 3 and~4, we first extract the context from the given
-  simpset and then print out a message containing the redex.  The function
+  arguments and prints out a message containing the redex.  The function
   returns @{ML NONE} (standing for an optional @{ML_type thm}) since at the
   moment we are \emph{not} interested in actually rewriting anything. We want
   that the simproc is triggered by the pattern @{term "Suc n"}. This can be
@@ -2518,15 +2517,15 @@
   Line 4 using the function @{ML_ind strip_abs_vars in Term}. For this we have to
   first transform the @{ML_type cterm} into a @{ML_type term}. In Line 5 we
   import these variables into the context \<open>ctxt'\<close>, in order to
-  export them again in Line 15.  In Line 8 we certify the list of variables,
+  export them again in Line 14.  In Line 7 we certify the list of variables,
   which in turn we apply to the @{ML_text lhs} of the definition using the
-  function @{ML_ind list_comb in Drule}. In Line 11 and 12 we generate the
+  function @{ML_ind list_comb in Drule}. In Line 10 and 11 we generate the
   conversion according to the length of the list of (abstracted) variables. If
   there are none, then we just return the conversion corresponding to the
   original definition. If there are variables, then we have to prefix this
-  conversion with @{ML_ind fun_conv in Conv}. Now in Line 14 we only have to
+  conversion with @{ML_ind fun_conv in Conv}. Now in Line 13 we only have to
   apply the new left-hand side to the generated conversion and obtain the the
-  theorem we want to construct. As mentioned above, in Line 15 we only have to
+  theorem we want to construct. As mentioned above, in Line 14 we only have to
   export the context \<open>ctxt'\<close> back to \<open>ctxt\<close> in order to 
   produce meta-variables for the theorem.  An example is as follows.