| changeset 60495 | d7ff0a1df90a |
| parent 59928 | b9b7f913a19a |
| child 60502 | aa58872267ee |
| child 60505 | 9e6584184315 |
--- a/src/HOL/Library/Tree_Multiset.thy Tue Jun 16 20:50:00 2015 +0100 +++ b/src/HOL/Library/Tree_Multiset.thy Wed Jun 17 17:21:11 2015 +0200 @@ -14,7 +14,7 @@ "mset_tree Leaf = {#}" | "mset_tree (Node l a r) = {#a#} + mset_tree l + mset_tree r" -lemma set_of_mset_tree[simp]: "set_of (mset_tree t) = set_tree t" +lemma set_mset_tree[simp]: "set_mset (mset_tree t) = set_tree t" by(induction t) auto lemma size_mset_tree[simp]: "size(mset_tree t) = size t"