src/HOL/Library/Multiset.thy
changeset 59997 90fb391a15c1
parent 59986 f38b94549dc8
child 59999 3fa68bacfa2b
--- 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