1057 

  1057 

  1058 text {*

  1058 text {*

  1059   will solve all trivial subgoals involving @{term True} or @{term "False"}.

  1059   will solve all trivial subgoals involving @{term True} or @{term "False"}.

  1060 

  1060 

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

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

  1062   

  1064   

  1063   \begin{readmore}

  1065   \begin{readmore}

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

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

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

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

  1066   \end{readmore}

  1068   \end{readmore}