1.1 --- a/src/HOL/Library/Mapping.thy	Wed Feb 17 13:48:13 2010 +0100
     1.2 +++ b/src/HOL/Library/Mapping.thy	Wed Feb 17 16:49:37 2010 +0100
     1.3 @@ -28,6 +28,9 @@
     1.4  definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where
     1.5    "keys m = dom (lookup m)"
     1.6  
     1.7 +definition ordered_keys :: "('a\<Colon>linorder, 'b) mapping \<Rightarrow> 'a list" where
     1.8 +  "ordered_keys m = sorted_list_of_set (keys m)"
     1.9 +
    1.10  definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool" where
    1.11    "is_empty m \<longleftrightarrow> dom (lookup m) = {}"
    1.12  
    1.13 @@ -139,6 +142,6 @@
    1.14    by (cases m) simp
    1.15  
    1.16  
    1.17 -hide (open) const empty is_empty lookup update delete keys size replace tabulate bulkload
    1.18 +hide (open) const empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
    1.19  
    1.20  end
    1.21 \ No newline at end of file