
diff -r 74c609115df0 -r 3f3223b90239 src/HOL/UNITY/Comp/AllocBase.thy
--- 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)"




