Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Lambda/ListBeta.thy
changeset 11183 0476c6e07bca
parent 10653 55f33da63366
child 11549 e7265e70fd7c 
--- a/src/HOL/Lambda/ListBeta.thy	Mon Feb 26 10:41:24 2001 +0100
+++ b/src/HOL/Lambda/ListBeta.thy	Mon Feb 26 16:36:53 2001 +0100
@@ -60,13 +60,13 @@
     apply (split split_if_asm)
      apply simp
      apply blast
-    apply (force intro: disjI1 [THEN append_step1I])
+    apply (force intro!: disjI1 [THEN append_step1I])
    apply (clarify del: disjCI)
    apply (drule App_eq_foldl_conv [THEN iffD1])
    apply (split split_if_asm)
     apply simp
     apply blast
-   apply (auto 0 3 intro: disjI2 [THEN append_step1I])
+   apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
   done
 
 lemma apps_betasE [elim!]:
isabelle