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.
Added two final lines to intro_tacsf for mutual recursion
authorlcp
Tue, 25 Jul 1995 17:01:25 +0200
changeset 1191 d7e0c280f261
parent 1190 9d1bdce3a38e
child 1192 d3a3cae80f08
Added two final lines to intro_tacsf for mutual recursion (borrowed from ZF version)
src/HOL/intr_elim.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/intr_elim.ML	Tue Jul 25 17:00:53 1995 +0200
+++ b/src/HOL/intr_elim.ML	Tue Jul 25 17:01:25 1995 +0200
@@ -85,7 +85,11 @@
    rtac disjIn 1,
    (*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] 1 ORELSE assume_tac 1)];
+   DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 ORELSE assume_tac 1),
+   (*Now solve the equations like Inl 0 = Inl ?b2*)
+   rewrite_goals_tac con_defs,
+   REPEAT (rtac refl 1)];
+
 
 (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
 val mk_disj_rls =
isabelle