--- a/CookBook/Tactical.thy	Fri Mar 13 16:57:16 2009 +0100
+++ b/CookBook/Tactical.thy	Sat Mar 14 00:48:22 2009 +0100
@@ -524,6 +524,7 @@
 
 text_raw{*
 \begin{figure}[t]
+\begin{minipage}{\textwidth}
 \begin{isabelle}
 *}
 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 
@@ -544,6 +545,7 @@
 end*}
 text_raw{*
 \end{isabelle}
+\end{minipage}
 \caption{A function that prints out the various parameters provided by the tactic
  @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for
   extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}}
@@ -1120,6 +1122,7 @@
 
 text_raw {*
 \begin{figure}[t]
+\begin{minipage}{\textwidth}
 \begin{isabelle}*}
 ML{*fun print_ss ctxt ss =
 let
@@ -1144,6 +1147,7 @@
 end*}
 text_raw {* 
 \end{isabelle}
+\end{minipage}
 \caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing
   all printable information stored in a simpset. We are here only interested in the 
   simplifcation rules, congruence rules and simprocs.\label{fig:printss}}
@@ -1455,7 +1459,7 @@
   done by adding the simproc to the current simpset as follows
 *}
 
-simproc_setup fail_sp ("Suc n") = {* K fail_sp_aux *}
+simproc_setup %gray fail_sp ("Suc n") = {* K fail_sp_aux *}
 
 text {*
   where the second argument specifies the pattern and the right-hand side
@@ -1539,7 +1543,7 @@
 *}
 
 lemma shows "Suc (Suc 0) = (Suc 1)"
-  apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail_sp']) 1*})
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail_sp']) 1*})
 (*<*)oops(*>*)
 
 text {*
@@ -1591,11 +1595,13 @@
 *}
 
 lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)"
-  apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one_sp]) 1*})
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one_sp]) 1*})
 txt{*
   where the simproc produces the goal state
-
+  
+  \begin{minipage}{\textwidth}
   @{subgoals[display]}
+  \end{minipage}
 *}  
 (*<*)oops(*>*)
 
@@ -1694,11 +1700,13 @@
   *}
 
 lemma "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
-  apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number_sp]) 1*})
+apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number_sp]) 1*})
 txt {* 
   you obtain the more legible goal state
   
+  \begin{minipage}{\textwidth}
   @{subgoals [display]}
+  \end{minipage}
   *}
 (*<*)oops(*>*)
 
@@ -2025,7 +2033,9 @@
 apply(tactic {* true1_tac 1 *})
 txt {* where the tactic yields the goal state
 
-       @{subgoals [display]}*}
+  \begin{minipage}{\textwidth}
+  @{subgoals [display]}
+  \end{minipage}*}
 (*<*)oops(*>*)
 
 text {*