equal
deleted
inserted
replaced
485 |
485 |
486 val refute_prems_tac = |
486 val refute_prems_tac = |
487 REPEAT(eresolve_tac [conjE, exE] 1 ORELSE |
487 REPEAT(eresolve_tac [conjE, exE] 1 ORELSE |
488 filter_prems_tac test 1 ORELSE |
488 filter_prems_tac test 1 ORELSE |
489 etac disjE 1) THEN |
489 etac disjE 1) THEN |
490 ref_tac 1; |
490 ((etac notE 1 THEN eq_assume_tac 1) ORELSE |
|
491 ref_tac 1); |
491 in EVERY'[TRY o filter_prems_tac test, |
492 in EVERY'[TRY o filter_prems_tac test, |
492 DETERM o REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac, |
493 DETERM o REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac, |
493 SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] |
494 SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] |
494 end; |
495 end; |