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 10653 55f33da63366
parent 9941 fe05af7ec816
child 11183 0476c6e07bca 
--- a/src/HOL/Lambda/ListBeta.thy	Wed Dec 13 09:30:59 2000 +0100
+++ b/src/HOL/Lambda/ListBeta.thy	Wed Dec 13 09:32:55 2000 +0100
@@ -47,23 +47,23 @@
      apply (case_tac r)
        apply simp
       apply (simp add: App_eq_foldl_conv)
-      apply (split (asm) split_if_asm)
+      apply (split split_if_asm)
        apply simp
        apply blast
       apply simp
      apply (simp add: App_eq_foldl_conv)
-     apply (split (asm) split_if_asm)
+     apply (split split_if_asm)
       apply simp
      apply simp
     apply (clarify del: disjCI)
     apply (drule App_eq_foldl_conv [THEN iffD1])
-    apply (split (asm) split_if_asm)
+    apply (split split_if_asm)
      apply simp
      apply blast
     apply (force intro: disjI1 [THEN append_step1I])
    apply (clarify del: disjCI)
    apply (drule App_eq_foldl_conv [THEN iffD1])
-   apply (split (asm) split_if_asm)
+   apply (split split_if_asm)
     apply simp
     apply blast
    apply (auto 0 3 intro: disjI2 [THEN append_step1I])
isabelle