diff -r cc3776f004e2 -r cbee04ce413b src/HOL/ex/InSort.thy --- a/src/HOL/ex/InSort.thy Sat Mar 26 00:00:56 2005 +0100 +++ b/src/HOL/ex/InSort.thy Sat Mar 26 00:01:56 2005 +0100 @@ -22,15 +22,15 @@ lemma multiset_ins[simp]: - "\y. multiset(ins le x xs) y = multiset (x#xs) y" -by (induct "xs") auto + "\y. multiset_of (ins le x xs) = multiset_of (x#xs)" + by (induct xs) (auto simp: union_ac) lemma insort_permutes[simp]: - "\x. multiset(insort le xs) x = multiset xs x"; -by (induct "xs") auto + "\x. multiset_of (insort le xs) = multiset_of xs" + by (induct "xs") auto lemma set_ins[simp]: "set(ins le x xs) = insert x (set xs)" -by (simp add: set_via_multiset) fast + by (simp add: set_count_greater_0) fast lemma sorted_ins[simp]: "\ total le; transf le \ \ sorted le (ins le x xs) = sorted le xs";