Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/simpdata.ML
changeset 6301 08245f5a436d
parent 6293 2a4357301973
child 6394 3d9fd50fcc43 
--- a/src/HOL/simpdata.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/simpdata.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -498,7 +498,7 @@
       val refute_prems_tac =
         REPEAT(eresolve_tac [conjE, exE] 1 ORELSE
                filter_prems_tac test 1 ORELSE
-               eresolve_tac [disjE] 1) THEN
+               etac disjE 1) THEN
         ref_tac 1;
   in EVERY'[TRY o filter_prems_tac test,
             DETERM o REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
isabelle