equal
deleted
inserted
replaced
417 |
417 |
418 local |
418 local |
419 |
419 |
420 fun meson_meth ctxt = |
420 fun meson_meth ctxt = |
421 Method.SIMPLE_METHOD' HEADGOAL |
421 Method.SIMPLE_METHOD' HEADGOAL |
422 (CHANGED_PROP o meson_claset_tac (Classical.get_local_claset ctxt)); |
422 (CHANGED_PROP o meson_claset_tac (local_claset_of ctxt)); |
423 |
423 |
424 val skolemize_meth = |
424 val skolemize_meth = |
425 Method.SIMPLE_METHOD' HEADGOAL |
425 Method.SIMPLE_METHOD' HEADGOAL |
426 (CHANGED_PROP o skolemize_tac); |
426 (CHANGED_PROP o skolemize_tac); |
427 |
427 |