1.1 --- a/src/HOL/ex/Bubblesort.thy	Thu Jun 18 16:17:51 2015 +0200
     1.2 +++ b/src/HOL/ex/Bubblesort.thy	Fri Jun 19 15:55:22 2015 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4      by(auto simp: size_bubble_min dest!: bubble_minD_size split: list.splits if_splits)
     1.5  qed
     1.6  
     1.7 -lemma mset_bubble_min: "multiset_of (bubble_min xs) = multiset_of xs"
     1.8 +lemma mset_bubble_min: "mset (bubble_min xs) = mset xs"
     1.9  apply(induction xs rule: bubble_min.induct)
    1.10    apply simp
    1.11   apply simp
    1.12 @@ -49,19 +49,19 @@
    1.13  done
    1.14  
    1.15  lemma bubble_minD_mset:
    1.16 -  "bubble_min (xs) = ys \<Longrightarrow> multiset_of xs = multiset_of ys"
    1.17 +  "bubble_min (xs) = ys \<Longrightarrow> mset xs = mset ys"
    1.18  by(auto simp: mset_bubble_min)
    1.19  
    1.20  lemma mset_bubblesort:
    1.21 -  "multiset_of (bubblesort xs) = multiset_of xs"
    1.22 +  "mset (bubblesort xs) = mset xs"
    1.23  apply(induction xs rule: bubblesort.induct)
    1.24    apply simp
    1.25   apply simp
    1.26  by(auto split: list.splits if_splits dest: bubble_minD_mset)
    1.27 -  (metis add_eq_conv_ex mset_bubble_min multiset_of.simps(2))
    1.28 +  (metis add_eq_conv_ex mset_bubble_min mset.simps(2))
    1.29  
    1.30  lemma set_bubblesort: "set (bubblesort xs) = set xs"
    1.31 -by(rule mset_bubblesort[THEN multiset_of_eq_setD])
    1.32 +by(rule mset_bubblesort[THEN mset_eq_setD])
    1.33  
    1.34  lemma bubble_min_min: "bubble_min xs = y#ys \<Longrightarrow> z \<in> set ys \<Longrightarrow> y \<le> z"
    1.35  apply(induction xs arbitrary: y ys z rule: bubble_min.induct)