1.1 --- a/src/HOL/Imperative_HOL/ex/Sublist.thy	Thu Jun 18 16:17:51 2015 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Fri Jun 19 15:55:22 2015 +0200
     1.3 @@ -471,26 +471,26 @@
     1.4  unfolding set_sublist' by blast
     1.5  
     1.6  
     1.7 -lemma multiset_of_sublist:
     1.8 +lemma mset_sublist:
     1.9  assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
    1.10  assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
    1.11  assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
    1.12 -assumes multiset: "multiset_of xs = multiset_of ys"
    1.13 -  shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)"
    1.14 +assumes multiset: "mset xs = mset ys"
    1.15 +  shows "mset (sublist' l r xs) = mset (sublist' l r ys)"
    1.16  proof -
    1.17    from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long") 
    1.18      by (simp add: sublist'_append)
    1.19 -  from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length)
    1.20 +  from multiset have length_eq: "List.length xs = List.length ys" by (rule mset_eq_length)
    1.21    with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long") 
    1.22      by (simp add: sublist'_append)
    1.23 -  from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp
    1.24 +  from xs_def ys_def multiset have "mset ?xs_long = mset ?ys_long" by simp
    1.25    moreover
    1.26    from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
    1.27      by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
    1.28    moreover
    1.29    from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
    1.30      by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
    1.31 -  ultimately show ?thesis by (simp add: multiset_of_append)
    1.32 +  ultimately show ?thesis by (simp add: mset_append)
    1.33  qed
    1.34  
    1.35