{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
--- a/src/ZF/indrule.ML Wed Sep 07 17:28:53 1994 +0200
+++ b/src/ZF/indrule.ML Thu Sep 08 11:05:06 1994 +0200
@@ -61,7 +61,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, iT-->oT);
@@ -75,7 +75,8 @@
(fn prems =>
[rtac (impI RS allI) 1,
etac raw_induct 1,
- REPEAT (FIRSTGOAL (eresolve_tac [CollectE,exE,conjE,disjE,ssubst])),
+ REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE, disjE] ORELSE'
+ hyp_subst_tac)),
REPEAT (FIRSTGOAL (eresolve_tac [PartE,CollectE])),
ind_tac (rev prems) (length prems) ]);
--- a/src/ZF/intr_elim.ML Wed Sep 07 17:28:53 1994 +0200
+++ b/src/ZF/intr_elim.ML Thu Sep 08 11:05:06 1994 +0200
@@ -92,7 +92,8 @@
REPEAT (resolve_tac [Part_eqI,CollectI] 1),
(*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
rtac disjIn 2,
- REPEAT (ares_tac [refl,exI,conjI] 2),
+ (*Not ares_tac, since refl must be tried before any equality assumptions*)
+ REPEAT (resolve_tac [refl,exI,conjI] 2 ORELSE assume_tac 2),
(*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
rewrite_goals_tac con_defs,
REPEAT (rtac refl 2),