equal
deleted
inserted
replaced
7 A tactic which solves all trivial cases in function |
7 A tactic which solves all trivial cases in function |
8 definitions, and leaves the others unchanged. |
8 definitions, and leaves the others unchanged. |
9 *} |
9 *} |
10 |
10 |
11 ML {* |
11 ML {* |
12 val all_trivials : (Proof.context -> Method.method) context_parser = |
12 val all_trivials : (Proof.context -> Proof.method) context_parser = |
13 Scan.succeed (fn ctxt => |
13 Scan.succeed (fn ctxt => |
14 let |
14 let |
15 val tac = TRYALL (SOLVED' (full_simp_tac ctxt)) |
15 val tac = TRYALL (SOLVED' (full_simp_tac ctxt)) |
16 in |
16 in |
17 Method.SIMPLE_METHOD' (K tac) |
17 Method.SIMPLE_METHOD' (K tac) |