author | haftmann |
Thu, 18 Feb 2010 08:17:12 +0100 | |
changeset 35196 | 6eab566aa609 |
parent 35195 | 5163c2d00904 |
child 35197 | 5c5457a7be85 |
--- a/src/HOL/Library/Tree.thy Wed Feb 17 16:49:38 2010 +0100 +++ b/src/HOL/Library/Tree.thy Thu Feb 18 08:17:12 2010 +0100 @@ -124,6 +124,9 @@ "Mapping.update k v (Tree t) = Tree (update k v t)" by (simp add: Tree_def lookup_update) +lemma [code, code del]: + "Mapping.ordered_keys = Mapping.ordered_keys " .. + lemma keys_Tree [code]: "Mapping.keys (Tree t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))" by (simp add: Mapping.keys_def lookup_Tree dom_lookup)