# HG changeset patch
# User lcp
# Date 779014905 -7200
# Node ID f745ff8bdb916fe5b3efbc3af2b4c24d45a1865b
# Parent  96c68fd7ed4626b50050c2775e845818fabfa70d
{HOL,ZF}/indrule/quant_induct: replaced ssubst in eresolve_tac by
separate call to hyp_subst_tac.  This avoids substituting in x=f(x)

{HOL,ZF}/indrule/ind_tac: now tries resolve_tac [refl].  This handles
trivial equalities such as x=a.

{HOL,ZF}/intr_elim/intro_tacsf_tac: now calls assume_tac last, to try refl
before any equality assumptions

diff -r 96c68fd7ed46 -r f745ff8bdb91 indrule.ML
--- a/indrule.ML	Wed Sep 07 13:17:34 1994 +0200
+++ b/indrule.ML	Thu Sep 08 11:01:45 1994 +0200
@@ -68,7 +68,7 @@
 
 (*Avoids backtracking by delivering the correct premise to each goal*)
 fun ind_tac [] 0 = all_tac
-  | ind_tac(prem::prems) i = REPEAT (ares_tac [Part_eqI,prem] i) THEN
+  | ind_tac(prem::prems) i = REPEAT (ares_tac [Part_eqI, prem, refl] i) THEN
 			     ind_tac prems (i-1);
 
 val pred = Free(pred_name, elem_type --> boolT);
@@ -82,8 +82,8 @@
       (fn prems =>
        [rtac (impI RS allI) 1,
 	etac raw_induct 1,
-	REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE, 
-					 ssubst])),
+	REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] 
+			   ORELSE' hyp_subst_tac)),
 	REPEAT (FIRSTGOAL (eresolve_tac [PartE, CollectE])),
 	ind_tac (rev prems) (length prems)])
     handle e => print_sign_exn sign e;
@@ -128,7 +128,7 @@
 	  (fn prems =>
 	   [cut_facts_tac prems 1,
 	    REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1
-	     ORELSE resolve_tac [allI, impI, conjI, Part_eqI] 1
+	     ORELSE resolve_tac [allI, impI, conjI, Part_eqI, refl] 1
 	     ORELSE dresolve_tac [spec, mp, splitD] 1)])
     handle e => print_sign_exn sign e;
 
diff -r 96c68fd7ed46 -r f745ff8bdb91 intr_elim.ML
--- a/intr_elim.ML	Wed Sep 07 13:17:34 1994 +0200
+++ b/intr_elim.ML	Thu Sep 08 11:01:45 1994 +0200
@@ -83,7 +83,8 @@
    REPEAT (resolve_tac [Part_eqI,CollectI] 1),
    (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
    rtac disjIn 1,
-   REPEAT (ares_tac [refl,exI,conjI] 1)];
+   (*Not ares_tac, since refl must be tried before any equality assumptions*)
+   REPEAT (resolve_tac [refl,exI,conjI] 1 ORELSE assume_tac 1)];
 
 (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
 val mk_disj_rls =