519   The combinators for instantiating theorems are defined in @{ML_file "Pure/drule.ML"}.

   519   The combinators for instantiating theorems are defined in @{ML_file "Pure/drule.ML"}.

   520   \end{readmore}

   520   \end{readmore}

   521 

   521 

   522   Often proofs on the ML-level involve elaborate operations on assumptions and 

   522   Often proofs on the ML-level involve elaborate operations on assumptions and 

   523   @{text "\<And>"}-quantified variables. To do such operations using the basic tactics 

   523   @{text "\<And>"}-quantified variables. To do such operations using the basic tactics 

   525   safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters 

   525   safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters 

   526   and binds the various components of a goal state to a record. 

   526   and binds the various components of a goal state to a record. 

   527   To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which

   527   To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which

   528   takes a record and just prints out the content of this record (using the 

   528   takes a record and just prints out the content of this record (using the 

   529   string transformation functions from in Section~\ref{sec:printing}). Consider

   529   string transformation functions from in Section~\ref{sec:printing}). Consider