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