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.
{HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
authorlcp
Wed, 12 Oct 1994 12:20:18 +0100
changeset 634 8a5f6961250f
parent 633 9e4d4f3eb812
child 635 034fda1c4873
{HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to solve the goal fully
src/ZF/intr_elim.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/intr_elim.ML	Wed Oct 12 12:09:54 1994 +0100
+++ b/src/ZF/intr_elim.ML	Wed Oct 12 12:20:18 1994 +0100
@@ -92,8 +92,9 @@
    REPEAT (resolve_tac [Part_eqI,CollectI] 1),
    (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
    rtac disjIn 2,
-   (*Not ares_tac, since refl must be tried before any equality assumptions*)
-   REPEAT (resolve_tac [refl,exI,conjI] 2 ORELSE assume_tac 2),
+   (*Not ares_tac, since refl must be tried before any equality assumptions;
+     backtracking may occur if the premises have extra variables!*)
+   DEPTH_SOLVE_1 (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),
isabelle