drop code lemma for ordered_keys
authorhaftmann
Thu, 18 Feb 2010 08:17:12 +0100
changeset 35196 6eab566aa609
parent 35195 5163c2d00904
child 35197 5c5457a7be85
drop code lemma for ordered_keys
src/HOL/Library/Tree.thy
--- 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)