arith_tac now copes with propositional reasoning as well.
--- 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)]