arith_tac now copes with propositional reasoning as well.
authornipkow
Fri Mar 09 19:05:48 2001 +0100 (2001-03-09)
changeset 11200f43fa07536c0
parent 11199 97cde35cec10
child 11201 eddc69b55fac
arith_tac now copes with propositional reasoning as well.
src/HOL/simpdata.ML
     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)]