4 

     5 

     6 text {*

     7   A tactic which solves all trivial cases in function 

     8   definitions, and leaves the others unchanged.

     9 *}

    10 

    11 ML {*

    12 val all_trivials : (Proof.context -> Method.method) context_parser =

    13 Scan.succeed (fn ctxt =>

    14  let

    15    val tac = TRYALL (SOLVED' (full_simp_tac (simpset_of ctxt)))

    16  in 

    17    Method.SIMPLE_METHOD' (K tac)

    18  end)

    19 *}

    20 

    21 method_setup all_trivials = {* all_trivials *} {* solves trivial goals *}