--- a/CookBook/Tactical.thy	Fri Feb 20 23:19:41 2009 +0000
+++ b/CookBook/Tactical.thy	Sat Feb 21 11:38:14 2009 +0000
@@ -521,7 +521,7 @@
 
   Often proofs on the ML-level involve elaborate operations on assumptions and 
   @{text "\<And>"}-quantified variables. To do such operations using the basic tactics 
-  is very unwieldy and brittle. Some convenience and
+  shown so far is very unwieldy and brittle. Some convenience and
   safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters 
   and binds the various components of a goal state to a record. 
   To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which