# HG changeset patch
# User lcp
# Date 775472603 -7200
# Node ID 612888a078894c265e26f5b765d86434d67f21c3
# Parent  3686157a5a514838cf0c5f79f086d7ca36a6abe0
ZF/intr_elim/intro_tacsf: now uses SigmaI as a default intro rule and
SigmaE2 as a default elim rule

diff -r 3686157a5a51 -r 612888a07889 src/ZF/intr_elim.ML
--- a/src/ZF/intr_elim.ML	Thu Jul 28 12:44:40 1994 +0200
+++ b/src/ZF/intr_elim.ML	Fri Jul 29 11:03:23 1994 +0200
@@ -252,10 +252,10 @@
    rewrite_goals_tac con_defs,
    (*Now can solve the trivial equation*)
    REPEAT (rtac refl 2),
-   REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::PartE::type_elims)
+   REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
 		      ORELSE' hyp_subst_tac
 		      ORELSE' dresolve_tac rec_typechecks)),
-   DEPTH_SOLVE (swap_res_tac type_intrs 1)];
+   DEPTH_SOLVE (swap_res_tac (SigmaI::type_intrs) 1)];
 
 (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
 val mk_disj_rls =