# HG changeset patch
# User nipkow
# Date 984161148 -3600
# Node ID f43fa07536c0e943551a5a0d9fba6ab6b5d0cccd
# Parent  97cde35cec1053826f2fa8beb62e356b00f2464f
arith_tac now copes with propositional reasoning as well.

diff -r 97cde35cec10 -r f43fa07536c0 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Mar 07 18:35:27 2001 +0100
+++ b/src/HOL/simpdata.ML	Fri Mar 09 19:05:48 2001 +0100
@@ -487,7 +487,8 @@
         REPEAT(eresolve_tac [conjE, exE] 1 ORELSE
                filter_prems_tac test 1 ORELSE
                etac disjE 1) THEN
-        ref_tac 1;
+        ((etac notE 1 THEN eq_assume_tac 1) ORELSE
+         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,
             SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]