diff -r ab606e685d52 -r 60da1ee5363f NEWS
--- a/NEWS	Fri Apr 13 12:49:33 2012 +0200
+++ b/NEWS	Fri Apr 13 13:29:55 2012 +0200
@@ -302,6 +302,116 @@
 * Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY,
 use theory HOL/Library/Nat_Bijection instead.
 
+* Theory HOL/Library/RBT_Impl: Backing implementation of red-black trees is
+now inside the type class' local context. Names of affected operations and lemmas 
+have been prefixed by rbt_. INCOMPATIBILITY for theories working directly with
+raw red-black trees, adapt the names as follows:
+
+  Operations:
+  bulkload -> rbt_bulkload
+  del_from_left -> rbt_del_from_left
+  del_from_right -> rbt_del_from_right
+  del -> rbt_del
+  delete -> rbt_delete
+  ins -> rbt_ins
+  insert -> rbt_insert
+  insertw -> rbt_insert_with
+  insert_with_key -> rbt_insert_with_key
+  map_entry -> rbt_map_entry
+  lookup -> rbt_lookup
+  sorted -> rbt_sorted
+  tree_greater -> rbt_greater
+  tree_less -> rbt_less
+  tree_less_symbol -> rbt_less_symbol
+  union -> rbt_union
+  union_with -> rbt_union_with
+  union_with_key -> rbt_union_with_key
+
+  Lemmas:
+  balance_left_sorted -> balance_left_rbt_sorted
+  balance_left_tree_greater -> balance_left_rbt_greater
+  balance_left_tree_less -> balance_left_rbt_less
+  balance_right_sorted -> balance_right_rbt_sorted
+  balance_right_tree_greater -> balance_right_rbt_greater
+  balance_right_tree_less -> balance_right_rbt_less
+  balance_sorted -> balance_rbt_sorted
+  balance_tree_greater -> balance_rbt_greater
+  balance_tree_less -> balance_rbt_less
+  bulkload_is_rbt -> rbt_bulkload_is_rbt
+  combine_sorted -> combine_rbt_sorted
+  combine_tree_greater -> combine_rbt_greater
+  combine_tree_less -> combine_rbt_less
+  delete_in_tree -> rbt_delete_in_tree
+  delete_is_rbt -> rbt_delete_is_rbt
+  del_from_left_tree_greater -> rbt_del_from_left_rbt_greater
+  del_from_left_tree_less -> rbt_del_from_left_rbt_less
+  del_from_right_tree_greater -> rbt_del_from_right_rbt_greater
+  del_from_right_tree_less -> rbt_del_from_right_rbt_less
+  del_in_tree -> rbt_del_in_tree
+  del_inv1_inv2 -> rbt_del_inv1_inv2
+  del_sorted -> rbt_del_rbt_sorted
+  del_tree_greater -> rbt_del_rbt_greater
+  del_tree_less -> rbt_del_rbt_less
+  dom_lookup_Branch -> dom_rbt_lookup_Branch
+  entries_lookup -> entries_rbt_lookup
+  finite_dom_lookup -> finite_dom_rbt_lookup
+  insert_sorted -> rbt_insert_rbt_sorted
+  insertw_is_rbt -> rbt_insertw_is_rbt
+  insertwk_is_rbt -> rbt_insertwk_is_rbt
+  insertwk_sorted -> rbt_insertwk_rbt_sorted
+  insertw_sorted -> rbt_insertw_rbt_sorted
+  ins_sorted -> ins_rbt_sorted
+  ins_tree_greater -> ins_rbt_greater
+  ins_tree_less -> ins_rbt_less
+  is_rbt_sorted -> is_rbt_rbt_sorted
+  lookup_balance -> rbt_lookup_balance
+  lookup_bulkload -> rbt_lookup_rbt_bulkload
+  lookup_delete -> rbt_lookup_rbt_delete
+  lookup_Empty -> rbt_lookup_Empty
+  lookup_from_in_tree -> rbt_lookup_from_in_tree
+  lookup_in_tree -> rbt_lookup_in_tree
+  lookup_ins -> rbt_lookup_ins
+  lookup_insert -> rbt_lookup_rbt_insert
+  lookup_insertw -> rbt_lookup_rbt_insertw
+  lookup_insertwk -> rbt_lookup_rbt_insertwk
+  lookup_keys -> rbt_lookup_keys
+  lookup_map -> rbt_lookup_map
+  lookup_map_entry -> rbt_lookup_rbt_map_entry
+  lookup_tree_greater -> rbt_lookup_rbt_greater
+  lookup_tree_less -> rbt_lookup_rbt_less
+  lookup_union -> rbt_lookup_rbt_union
+  map_entry_color_of -> rbt_map_entry_color_of
+  map_entry_inv1 -> rbt_map_entry_inv1
+  map_entry_inv2 -> rbt_map_entry_inv2
+  map_entry_is_rbt -> rbt_map_entry_is_rbt
+  map_entry_sorted -> rbt_map_entry_rbt_sorted
+  map_entry_tree_greater -> rbt_map_entry_rbt_greater
+  map_entry_tree_less -> rbt_map_entry_rbt_less
+  map_tree_greater -> map_rbt_greater
+  map_tree_less -> map_rbt_less
+  map_sorted -> map_rbt_sorted
+  paint_sorted -> paint_rbt_sorted
+  paint_lookup -> paint_rbt_lookup
+  paint_tree_greater -> paint_rbt_greater
+  paint_tree_less -> paint_rbt_less
+  sorted_entries -> rbt_sorted_entries
+  tree_greater_eq_trans -> rbt_greater_eq_trans
+  tree_greater_nit -> rbt_greater_nit
+  tree_greater_prop -> rbt_greater_prop
+  tree_greater_simps -> rbt_greater_simps
+  tree_greater_trans -> rbt_greater_trans
+  tree_less_eq_trans -> rbt_less_eq_trans
+  tree_less_nit -> rbt_less_nit
+  tree_less_prop -> rbt_less_prop
+  tree_less_simps -> rbt_less_simps
+  tree_less_trans -> rbt_less_trans
+  tree_ord_props -> rbt_ord_props
+  union_Branch -> rbt_union_Branch
+  union_is_rbt -> rbt_union_is_rbt
+  unionw_is_rbt -> rbt_unionw_is_rbt
+  unionwk_is_rbt -> rbt_unionwk_is_rbt
+  unionwk_sorted -> rbt_unionwk_rbt_sorted
+
 * Session HOL-Word: Discontinued many redundant theorems specific to
 type 'a word. INCOMPATIBILITY, use the corresponding generic theorems
 instead.