# HG changeset patch
# User wenzelm
# Date 1428659575 -7200
# Node ID 90fb391a15c12e64e170b58bcab91c77e6c99368
# Parent  4dca485579216fd95196defd9856cb29cb051cfe
tuned proofs;

diff -r 4dca48557921 -r 90fb391a15c1 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Apr 10 11:31:10 2015 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Apr 10 11:52:55 2015 +0200
@@ -2438,8 +2438,7 @@
     unfolding rel_mset_def[abs_def] BNF_Def.Grp_def OO_def
     apply (rule ext)+
     apply auto
-     apply (rule_tac x = "multiset_of (zip xs ys)" in exI)
-     apply auto[1]
+     apply (rule_tac x = "multiset_of (zip xs ys)" in exI; auto)
         apply (metis list_all2_lengthD map_fst_zip multiset_of_map)
        apply (auto simp: list_all2_iff)[1]
       apply (metis list_all2_lengthD map_snd_zip multiset_of_map)
@@ -2451,7 +2450,8 @@
     apply (rule_tac x = "map fst xys" in exI)
     apply (auto simp: multiset_of_map)
     apply (rule_tac x = "map snd xys" in exI)
-    by (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd)
+    apply (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd)
+    done
 next
   show "\<And>z. z \<in> set_of {#} \<Longrightarrow> False"
     by auto
diff -r 4dca48557921 -r 90fb391a15c1 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Fri Apr 10 11:31:10 2015 +0200
+++ b/src/HOL/Library/Sublist.thy	Fri Apr 10 11:52:55 2015 +0200
@@ -144,7 +144,7 @@
 
 lemma take_prefix: "prefix xs ys \<Longrightarrow> prefix (take n xs) ys"
   apply (induct n arbitrary: xs ys)
-   apply (case_tac ys, simp_all)[1]
+   apply (case_tac ys; simp)
   apply (metis prefix_order.less_trans prefixI take_is_prefixeq)
   done