changeset 11200 | f43fa07536c0 |
parent 11162 | 9e2ec5f02217 |
child 11220 | db536a42dfc5 |
1.1 --- a/src/HOL/simpdata.ML Wed Mar 07 18:35:27 2001 +0100 1.2 +++ b/src/HOL/simpdata.ML Fri Mar 09 19:05:48 2001 +0100 1.3 @@ -487,7 +487,8 @@ 1.4 REPEAT(eresolve_tac [conjE, exE] 1 ORELSE 1.5 filter_prems_tac test 1 ORELSE 1.6 etac disjE 1) THEN 1.7 - ref_tac 1; 1.8 + ((etac notE 1 THEN eq_assume_tac 1) ORELSE 1.9 + ref_tac 1); 1.10 in EVERY'[TRY o filter_prems_tac test, 1.11 DETERM o REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac, 1.12 SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]