| changeset 3218 | 89158f401b07 |
| parent 3191 | 0440bc1a2438 |
| child 3230 | b33b42211bbf |
| 3217:d67a6a48f1c7 | 3218:89158f401b07 |
|---|---|
10 |
10 |
11 ML {* |
11 ML {* |
12 val all_trivials : (Proof.context -> Method.method) context_parser = |
12 val all_trivials : (Proof.context -> Method.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 (simpset_of 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) |
18 end) |
18 end) |
19 *} |
19 *} |
20 |
20 |