396       @{subgoals [display]}

   396       @{subgoals [display]}

   397       \end{minipage}*}

   397       \end{minipage}*}

   398 (*<*)oops(*>*)

   398 (*<*)oops(*>*)

   399 

   399 

   400 text {*

   400 text {*

   403   The function @{ML resolve_tac} is similar to @{ML rtac}, except that it

   401   The function @{ML resolve_tac} is similar to @{ML rtac}, except that it

   404   expects a list of theorems as arguments. From this list it will apply the

   402   expects a list of theorems as arguments. From this list it will apply the

   405   first applicable theorem (later theorems that are also applicable can be

   403   first applicable theorem (later theorems that are also applicable can be

   406   explored via the lazy sequences mechanism). Given the code

   404   explored via the lazy sequences mechanism). Given the code

   407 *}

   405 *}