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.
intro_tacsf now includes subsetI as an introduction rule. It is
authorlcp
Mon, 27 Feb 1995 17:44:43 +0100
changeset 909 5de21942d046
parent 908 1f99a44c10cb
child 910 822e57491612
intro_tacsf now includes subsetI as an introduction rule. It is needed for rules like list_into_univ
src/ZF/intr_elim.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/intr_elim.ML	Mon Feb 27 17:40:57 1995 +0100
+++ b/src/ZF/intr_elim.ML	Mon Feb 27 17:44:43 1995 +0100
@@ -110,7 +110,7 @@
    REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
 		      ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
 		      ORELSE' hyp_subst_tac)),
-   DEPTH_SOLVE (swap_res_tac (SigmaI::type_intrs) 1)];
+   DEPTH_SOLVE (swap_res_tac (SigmaI::subsetI::type_intrs) 1)];
 
 (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
 val mk_disj_rls =
isabelle