--- a/src/HOL/Library/Multiset.thy Tue Nov 07 14:02:08 2006 +0100
+++ b/src/HOL/Library/Multiset.thy Tue Nov 07 14:02:10 2006 +0100
@@ -259,11 +259,11 @@
lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
by (simp add: multiset_eq_conv_count_eq multiset_inter_count
- min_max.below_inf.inf_commute)
+ min_max.inf_commute)
lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
by (simp add: multiset_eq_conv_count_eq multiset_inter_count
- min_max.below_inf.inf_assoc)
+ min_max.inf_assoc)
lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
by (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def)