adjusted two lemma names due to name change in interpretation
authorhaftmann
Tue, 07 Nov 2006 14:02:10 +0100
changeset 21214 a91bab12b2bd
parent 21213 c81f016883df
child 21215 7c9337a0e30a
adjusted two lemma names due to name change in interpretation
src/HOL/Library/Multiset.thy
--- 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)