--- a/src/HOL/Library/Tree_Multiset.thy Mon Jul 27 23:56:11 2015 +0200
+++ b/src/HOL/Library/Tree_Multiset.thy Tue Jul 28 13:00:54 2015 +0200
@@ -35,9 +35,4 @@
lemma map_mirror: "mset_tree (mirror t) = mset_tree t"
by (induction t) (simp_all add: ac_simps)
-lemma del_rightmost_mset_tree:
- "\<lbrakk> del_rightmost t = (t',x); t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> mset_tree t = {#x#} + mset_tree t'"
-apply(induction t arbitrary: t' rule: del_rightmost.induct)
-by (auto split: prod.splits) (auto simp: ac_simps)
-
end