Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ZF/intr_elim/intro_tacsf: now uses SigmaI as a default intro rule and
authorlcp
Fri, 29 Jul 1994 11:03:23 +0200
changeset 495 612888a07889
parent 494 3686157a5a51
child 496 3fc829fa81d2
ZF/intr_elim/intro_tacsf: now uses SigmaI as a default intro rule and SigmaE2 as a default elim rule
src/ZF/intr_elim.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle