| changeset 63409 | 3f3223b90239 |
| parent 63388 | a095acd4cfbf |
| child 63410 | 9789ccc2a477 |
--- a/src/HOL/UNITY/Comp/AllocBase.thy Thu Jul 07 00:43:27 2016 +0200 +++ b/src/HOL/UNITY/Comp/AllocBase.thy Thu Jul 07 09:24:03 2016 +0200 @@ -39,7 +39,6 @@ lemma subseteq_le_multiset: "(A :: 'a::order multiset) \<le> A + B" unfolding less_eq_multiset_def apply (cases B; simp) apply (rule union_le_mono2[of "{#}" "_ + {#_#}" A, simplified]) -apply (simp add: less_multiset\<^sub>H\<^sub>O) done lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"