src/HOL/simpdata.ML
changeset 6301 08245f5a436d
parent 6293 2a4357301973
child 6394 3d9fd50fcc43
     1.1 --- a/src/HOL/simpdata.ML	Wed Mar 03 11:12:29 1999 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Mar 03 11:15:18 1999 +0100
     1.3 @@ -498,7 +498,7 @@
     1.4        val refute_prems_tac =
     1.5          REPEAT(eresolve_tac [conjE, exE] 1 ORELSE
     1.6                 filter_prems_tac test 1 ORELSE
     1.7 -               eresolve_tac [disjE] 1) THEN
     1.8 +               etac disjE 1) THEN
     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,