--- a/CookBook/Tactical.thy	Thu Mar 12 15:43:22 2009 +0000
+++ b/CookBook/Tactical.thy	Thu Mar 12 18:39:10 2009 +0000
@@ -165,7 +165,7 @@
 
 text {*
   which means @{ML no_tac} always fails. The second returns the given theorem wrapped 
-  up in a single member sequence; it is defined as
+  in a single member sequence; it is defined as
 *}
 
 ML{*fun all_tac thm = Seq.single thm*}
@@ -216,6 +216,7 @@
 
 text_raw {*
   \begin{figure}[p]
+  \begin{boxedminipage}{\textwidth}
   \begin{isabelle}
 *}
 lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B" 
@@ -284,10 +285,11 @@
 done
 text_raw {*  
   \end{isabelle}
+  \end{boxedminipage}
   \caption{The figure shows a proof where each intermediate goal state is
   printed by the Isabelle system and by @{ML my_print_tac}. The latter shows
   the goal state as represented internally (highlighted boxes). This
-  illustrates that every goal state in Isabelle is represented by a theorem:
+  tactic shows that every goal state in Isabelle is represented by a theorem:
   when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is
   @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the
   theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}}
@@ -326,10 +328,10 @@
 section {* Simple Tactics *}
 
 text {*
-  Let us start with the tactic @{ML print_tac}, which is quite useful for low-level 
-  debugging of tactics. It just prints out a message and the current goal state 
-  (unlike @{ML my_print_tac}, it prints the goal state as the user would see it). 
-  For example, processing the proof
+  Let us start with explaining the simple tactic @{ML print_tac}, which is quite useful 
+  for low-level debugging of tactics. It just prints out a message and the current 
+  goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state 
+  as the user would see it.  For example, processing the proof
 *}
  
 lemma shows "False \<Longrightarrow> True"
@@ -386,9 +388,9 @@
 
 text {*
   Note the number in each tactic call. Also as mentioned in the previous section, most 
-  basic tactics take such a number as argument; it addresses the subgoal they are analysing. 
-  In the proof below, we first split up the conjunction in  the second subgoal by 
-  focusing on this subgoal first.
+  basic tactics take such a number as argument: this argument addresses the subgoal 
+  the tacics are analysing. In the proof below, we first split up the conjunction in  
+  the second subgoal by focusing on this subgoal first.
 *}
 
 lemma shows "Foo" and "P \<and> Q"
@@ -421,7 +423,7 @@
 (*<*)oops(*>*)
 
 text {* 
-  Similarly versions taking a list of theorems exist for the tactics 
+  Similarl versions taking a list of theorems exist for the tactics 
   @{ML dtac} (@{ML dresolve_tac}), @{ML etac} (@{ML eresolve_tac}) and so on.
 
 
@@ -521,7 +523,7 @@
 *}
 
 text_raw{*
-\begin{figure}
+\begin{figure}[t]
 \begin{isabelle}
 *}
 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 
@@ -1117,7 +1119,7 @@
 *}
 
 text_raw {*
-\begin{figure}[tp]
+\begin{figure}[t]
 \begin{isabelle}*}
 ML{*fun print_ss ctxt ss =
 let
@@ -1265,7 +1267,8 @@
 
 
 text_raw {*
-\begin{figure}[tp]
+\begin{figure}[p]
+\begin{boxedminipage}{\textwidth}
 \begin{isabelle} *}
 types  prm = "(nat \<times> nat) list"
 consts perm :: "prm \<Rightarrow> 'a \<Rightarrow> 'a"  ("_ \<bullet> _" [80,80] 80)
@@ -1302,7 +1305,8 @@
   shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>(pi\<^isub>1\<bullet>c)" 
 by (induct pi\<^isub>2) (auto)
 text_raw {*
-\end{isabelle}\medskip
+\end{isabelle}
+\end{boxedminipage}
 \caption{A simple theory about permutations over @{typ nat}. The point is that the
   lemma @{thm [source] perm_compose} cannot be directly added to the simplifier, as
   it would cause the simplifier to loop. It can still be used as a simplification