equal
deleted
inserted
replaced
4411 by (cases "x \<in># M") (simp_all add: size_Diff1_less less_imp_le diff_single_trivial) |
4411 by (cases "x \<in># M") (simp_all add: size_Diff1_less less_imp_le diff_single_trivial) |
4412 |
4412 |
4413 lemma size_psubset: "M \<subseteq># M' \<Longrightarrow> size M < size M' \<Longrightarrow> M \<subset># M'" |
4413 lemma size_psubset: "M \<subseteq># M' \<Longrightarrow> size M < size M' \<Longrightarrow> M \<subset># M'" |
4414 using less_irrefl subset_mset_def by blast |
4414 using less_irrefl subset_mset_def by blast |
4415 |
4415 |
|
4416 lifting_update multiset.lifting |
|
4417 lifting_forget multiset.lifting |
|
4418 |
4416 hide_const (open) wcount |
4419 hide_const (open) wcount |
4417 |
4420 |
4418 end |
4421 end |