equal
deleted
inserted
replaced
381 (* proof method setup *) |
381 (* proof method setup *) |
382 |
382 |
383 local |
383 local |
384 |
384 |
385 fun meson_meth ctxt = |
385 fun meson_meth ctxt = |
386 Method.SIMPLE_METHOD' HEADGOAL (CHANGED o meson_claset_tac (Classical.get_local_claset ctxt)); |
386 Method.SIMPLE_METHOD' HEADGOAL |
|
387 (CHANGED_PROP o meson_claset_tac (Classical.get_local_claset ctxt)); |
387 |
388 |
388 in |
389 in |
389 |
390 |
390 val meson_setup = |
391 val meson_setup = |
391 [Method.add_methods |
392 [Method.add_methods |