src/HOL/Library/Multiset.thy
changeset 59997 90fb391a15c1
parent 59986 f38b94549dc8
child 59999 3fa68bacfa2b
     1.1 --- a/src/HOL/Library/Multiset.thy	Fri Apr 10 11:31:10 2015 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Apr 10 11:52:55 2015 +0200
     1.3 @@ -2438,8 +2438,7 @@
     1.4      unfolding rel_mset_def[abs_def] BNF_Def.Grp_def OO_def
     1.5      apply (rule ext)+
     1.6      apply auto
     1.7 -     apply (rule_tac x = "multiset_of (zip xs ys)" in exI)
     1.8 -     apply auto[1]
     1.9 +     apply (rule_tac x = "multiset_of (zip xs ys)" in exI; auto)
    1.10          apply (metis list_all2_lengthD map_fst_zip multiset_of_map)
    1.11         apply (auto simp: list_all2_iff)[1]
    1.12        apply (metis list_all2_lengthD map_snd_zip multiset_of_map)
    1.13 @@ -2451,7 +2450,8 @@
    1.14      apply (rule_tac x = "map fst xys" in exI)
    1.15      apply (auto simp: multiset_of_map)
    1.16      apply (rule_tac x = "map snd xys" in exI)
    1.17 -    by (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd)
    1.18 +    apply (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd)
    1.19 +    done
    1.20  next
    1.21    show "\<And>z. z \<in> set_of {#} \<Longrightarrow> False"
    1.22      by auto