1058   (FIXME: say something about @{ML [index] COND} and COND')

  1058   (FIXME: say something about @{ML [index] COND} and COND')

  1059   

  1059   

  1060   \begin{readmore}

  1060   \begin{readmore}

  1061   Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}.

  1061   Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}.

  1062   Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}.

  1062   Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}.

  1064   \end{readmore}

  1063   \end{readmore}

  1065 

  1064 

  1066 *}

  1065 *}

  1067 

  1066 

  1068 section {* Simplifier Tactics *}

  1067 section {* Simplifier Tactics *}