src/Pure/General/table.ML
changeset 16887 b24c067b32d6
parent 16864 0f536ece46e3
child 16894 40f80823b451
     1.1 --- a/src/Pure/General/table.ML	Tue Jul 19 17:21:58 2005 +0200
     1.2 +++ b/src/Pure/General/table.ML	Tue Jul 19 17:21:59 2005 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4    val max_key: 'a table -> key option
     1.5    val exists: (key * 'a -> bool) -> 'a table -> bool
     1.6    val forall: (key * 'a -> bool) -> 'a table -> bool
     1.7 +  val defined: 'a table -> key -> bool
     1.8    val lookup: 'a table * key -> 'a option
     1.9    val update: (key * 'a) * 'a table -> 'a table
    1.10    val update_new: (key * 'a) * 'a table -> 'a table                    (*exception DUP*)
    1.11 @@ -145,6 +146,8 @@
    1.12            | EQUAL => SOME x2
    1.13            | GREATER => lookup (right, key)));
    1.14  
    1.15 +fun defined tab key = is_some (lookup (tab, key));
    1.16 +
    1.17  
    1.18  (* updates *)
    1.19