633   \texttt{quant}, which may be, for example,

   633   \texttt{quant}, which may be, for example,

   634   \texttt{ALLGOALS} (all subgoals),

   634   \texttt{ALLGOALS} (all subgoals),

   635   \texttt{TRYALL} (try all subgoals, failure is OK),

   635   \texttt{TRYALL} (try all subgoals, failure is OK),

   636   \texttt{FIRSTGOAL} (try subgoals until it succeeds once), 

   636   \texttt{FIRSTGOAL} (try subgoals until it succeeds once), 

   637   \texttt{(fn tacf => tacf 4)} (subgoal 4), etc

   637   \texttt{(fn tacf => tacf 4)} (subgoal 4), etc

   639 

   639 

   640   A method is stored in a theory as indicated by:

   640   A method is stored in a theory as indicated by:

   641   \begin{verbatim}

   641   \begin{verbatim}

   642   Method.add_method : 

   642   Method.add_method : 

   643   (bstring * (src -> Proof.context -> method) * string) -> theory trf ; 

   643   (bstring * (src -> Proof.context -> method) * string) -> theory trf ;