# HG changeset patch
# User paulson
# Date 881919465 -3600
# Node ID ea41d9c1b0efc37177a93907c511621d391e17a8
# Parent  cc3e8453d7f010ce587862c33c4c1a82b66b5cf0
More deterministic (?) contr_tac

diff -r cc3e8453d7f0 -r ea41d9c1b0ef src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Dec 12 10:34:21 1997 +0100
+++ b/src/Provers/classical.ML	Fri Dec 12 10:37:45 1997 +0100
@@ -174,8 +174,11 @@
 val imp_elim = (*cannot use bind_thm within a structure!*)
   store_thm ("imp_elim", make_elim mp);
 
-(*Solve goal that assumes both P and ~P. *)
-val contr_tac = eresolve_tac [not_elim]  THEN'  assume_tac;
+(*Prove goal that assumes both P and ~P.  
+  No backtracking if it finds an equal assumption.  Perhaps should call
+  ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*)
+val contr_tac = eresolve_tac [not_elim]  THEN'  
+                (eq_assume_tac ORELSE' assume_tac);
 
 (*Finds P-->Q and P in the assumptions, replaces implication by Q.
   Could do the same thing for P<->Q and P... *)