1064 

  1064 

  1065   (FIXME: read a name and show how to store theorems; see @{ML_ind  note in LocalTheory})

  1065   (FIXME: read a name and show how to store theorems; see @{ML_ind  note in LocalTheory})

  1066   

  1066   

  1067 *}

  1067 *}

  1068 

  1068 

  1069 section {* Methods (TBD) *}

  1072 section {* Methods (TBD) *}

  1070 

  1073 

  1071 text {*

  1074 text {*

  1072   (FIXME: maybe move to after the tactic section)

  1075   (FIXME: maybe move to after the tactic section)

  1073 

  1076 

  1106 

  1109 

  1107   \begin{minipage}{\textwidth}

  1110   \begin{minipage}{\textwidth}

  1108   @{subgoals}

  1111   @{subgoals}

  1109   \end{minipage} *}

  1112   \end{minipage} *}

  1110 (*<*)oops(*>*)

  1113 (*<*)oops(*>*)

  1111 

  1118 

  1112 

  1119 

  1113 (*

  1120 (*

  1114 ML {* SIMPLE_METHOD *}

  1121 ML {* SIMPLE_METHOD *}

  1115 ML {* METHOD *}

  1122 ML {* METHOD *}