--- a/ProgTutorial/Tactical.thy	Tue Mar 24 18:06:20 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Wed Mar 25 15:09:04 2009 +0100
@@ -515,7 +515,8 @@
   theorem in the first.
 
   @{ML_response_fake [display,gray]
-   "[@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}]" 
+"map (no_vars @{context}) 
+   ([@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}])" 
 "[\<lbrakk>P \<Longrightarrow> Q; Qa\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> Qa,
  \<lbrakk>Q; Qa\<rbrakk> \<Longrightarrow> (P \<or> Q) \<and> Qa,
  (P \<Longrightarrow> Q) \<Longrightarrow> (P \<longrightarrow> Q) \<or> Qa,
@@ -1067,7 +1068,7 @@
 
 text {*
   If the simplifier cannot make any progress, then it leaves the goal unchanged,
-  i.e.~does not raise any error message. That means if you use it to unfold a 
+  i.e., does not raise any error message. That means if you use it to unfold a 
   definition for a constant and this constant is not present in the goal state, 
   you can still safely apply the simplifier.
 
@@ -1117,11 +1118,11 @@
   \end{readmore}
 
   \begin{readmore}
-  FIXME: Find the right place Discrimination nets are implemented
+  FIXME: Find the right place: Discrimination nets are implemented
   in @{ML_file "Pure/net.ML"}.
   \end{readmore}
 
-  The most common combinators to modify simpsets are
+  The most common combinators to modify simpsets are:
 
   \begin{isabelle}
   \begin{tabular}{ll}
@@ -1170,7 +1171,7 @@
 text {* 
   To see how they work, consider the function in Figure~\ref{fig:printss}, which
   prints out some parts of a simpset. If you use it to print out the components of the
-  empty simpset, i.e.~ @{ML empty_ss}
+  empty simpset, i.e., @{ML empty_ss}
   
   @{ML_response_fake [display,gray]
   "print_ss @{context} empty_ss"
@@ -1351,7 +1352,7 @@
   it would be desirable to add also the lemma @{thm [source] perm_compose} to
   the simplifier for pushing permutations over other permutations. Unfortunately, 
   the right-hand side of this lemma is again an instance of the left-hand side 
-  and so causes an infinite loop. The seems to be no easy way to reformulate 
+  and so causes an infinite loop. There seems to be no easy way to reformulate 
   this rule and so one ends up with clunky proofs like:
 *}
 
@@ -1417,7 +1418,7 @@
 end*}
 
 text {*
-  For all three phases we have to build simpsets addig specific lemmas. As is sufficient
+  For all three phases we have to build simpsets adding specific lemmas. As is sufficient
   for our purposes here, we can add these lemma to @{ML HOL_basic_ss} in order to obtain
   the desired results. Now we can solve the following lemma
 *}
@@ -1430,8 +1431,8 @@
 
 
 text {*
-  in one step. This tactic can deal with most instances of normalising permutations;
-  in order to solve all cases we have to deal with corner-cases such as the
+  in one step. This tactic can deal with most instances of normalising permutations.
+  In order to solve all cases we have to deal with corner-cases such as the
   lemma being an exact instance of the permutation composition lemma. This can
   often be done easier by implementing a simproc or a conversion. Both will be 
   explained in the next two chapters.