--- a/src/HOL/Library/Mapping.thy Wed Feb 17 13:48:13 2010 +0100
+++ b/src/HOL/Library/Mapping.thy Wed Feb 17 16:49:37 2010 +0100
@@ -28,6 +28,9 @@
definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where
"keys m = dom (lookup m)"
+definition ordered_keys :: "('a\<Colon>linorder, 'b) mapping \<Rightarrow> 'a list" where
+ "ordered_keys m = sorted_list_of_set (keys m)"
+
definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool" where
"is_empty m \<longleftrightarrow> dom (lookup m) = {}"
@@ -139,6 +142,6 @@
by (cases m) simp
-hide (open) const empty is_empty lookup update delete keys size replace tabulate bulkload
+hide (open) const empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
end
\ No newline at end of file