diff -r 74846cb0fff9 -r 693711a0c702 CookBook/Tactical.thy --- 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 "\"}-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