src/HOL/Library/Multiset.thy
changeset 36635 080b755377c0
parent 36176 3fe7e97ccca8
child 36867 6c28c702ed22
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue May 04 08:55:39 2010 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue May 04 08:55:43 2010 +0200
     1.3 @@ -1239,7 +1239,7 @@
     1.4    qed
     1.5    have trans: "\<And>K M N :: 'a multiset. K \<subset># M \<Longrightarrow> M \<subset># N \<Longrightarrow> K \<subset># N"
     1.6      unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
     1.7 -  show "order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
     1.8 +  show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
     1.9    qed (auto simp add: le_multiset_def irrefl dest: trans)
    1.10  qed
    1.11