equal
deleted
inserted
replaced
4 |
4 |
5 theory Tree_Multiset |
5 theory Tree_Multiset |
6 imports Multiset Tree |
6 imports Multiset Tree |
7 begin |
7 begin |
8 |
8 |
9 text\<open>Kept separate from theory @{theory Tree} to avoid importing all of |
9 text \<open> |
10 theory @{theory Multiset} into @{theory Tree}. Should be merged if |
10 Kept separate from theory @{theory "HOL-Library.Tree"} to avoid importing all of theory @{theory |
11 @{theory Multiset} ever becomes part of @{theory Main}.\<close> |
11 "HOL-Library.Multiset"} into @{theory "HOL-Library.Tree"}. Should be merged if @{theory |
|
12 "HOL-Library.Multiset"} ever becomes part of @{theory Main}. |
|
13 \<close> |
12 |
14 |
13 fun mset_tree :: "'a tree \<Rightarrow> 'a multiset" where |
15 fun mset_tree :: "'a tree \<Rightarrow> 'a multiset" where |
14 "mset_tree Leaf = {#}" | |
16 "mset_tree Leaf = {#}" | |
15 "mset_tree (Node l a r) = {#a#} + mset_tree l + mset_tree r" |
17 "mset_tree (Node l a r) = {#a#} + mset_tree l + mset_tree r" |
16 |
18 |