tuned proofs;
authorwenzelm
Fri Apr 10 11:52:55 2015 +0200 (2015-04-10)
changeset 5999790fb391a15c1
parent 59996 4dca48557921
child 59999 3fa68bacfa2b
tuned proofs;
src/HOL/Library/Multiset.thy
src/HOL/Library/Sublist.thy
     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
     2.1 --- a/src/HOL/Library/Sublist.thy	Fri Apr 10 11:31:10 2015 +0200
     2.2 +++ b/src/HOL/Library/Sublist.thy	Fri Apr 10 11:52:55 2015 +0200
     2.3 @@ -144,7 +144,7 @@
     2.4  
     2.5  lemma take_prefix: "prefix xs ys \<Longrightarrow> prefix (take n xs) ys"
     2.6    apply (induct n arbitrary: xs ys)
     2.7 -   apply (case_tac ys, simp_all)[1]
     2.8 +   apply (case_tac ys; simp)
     2.9    apply (metis prefix_order.less_trans prefixI take_is_prefixeq)
    2.10    done
    2.11