# HG changeset patch # User lcp # Date 785758435 -3600 # Node ID f0aacbcedb777f2ad6d39263091a37d23215d842 # Parent 019aadf0e3156dced34acda3067612436c9b5b99 ZF/indrule/mutual_ind_tac: ensured that asm_full_simp_tac ignores any equalities, by adding setmksimps K[]. ZF/indrule/mut_ss: removed Collect_cong; it is redundant. diff -r 019aadf0e315 -r f0aacbcedb77 src/ZF/indrule.ML --- a/src/ZF/indrule.ML Fri Nov 25 11:08:12 1994 +0100 +++ b/src/ZF/indrule.ML Fri Nov 25 11:13:55 1994 +0100 @@ -139,8 +139,7 @@ (*Simplification largely reduces the mutual induction rule to the standard rule*) val mut_ss = - FOL_ss addcongs [Collect_cong] - addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff]; + FOL_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff]; val all_defs = con_defs@part_rec_defs; @@ -159,17 +158,19 @@ (SELECT_GOAL ( (*Simplify the assumptions and goal by unfolding Part and - using freeness of the Sum constructors*) + using freeness of the Sum constructors; proves all but one + conjunct by contradiction*) rewrite_goals_tac all_defs THEN simp_tac (mut_ss addsimps [Part_iff]) 1 THEN IF_UNSOLVED (*simp_tac may have finished it off!*) - (asm_full_simp_tac mut_ss 1 THEN + ((*simplify assumptions, but don't accept new rewrite rules!*) + asm_full_simp_tac (mut_ss setmksimps K[]) 1 THEN (*unpackage and use "prem" in the corresponding place*) REPEAT (rtac impI 1) THEN rtac (rewrite_rule all_defs prem) 1 THEN (*prem must not be REPEATed below: could loop!*) DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' - eresolve_tac ([conjE]@cmonos)))) + eresolve_tac (conjE::mp::cmonos)))) ) i) THEN mutual_ind_tac prems (i-1);