src/HOL/Data_Structures/RBT_Set.thy

 theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
 by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint)
 
 text \<open>Overall correctness:\<close>
 
-interpretation Set_by_Ordered
+interpretation S: Set_by_Ordered
 where empty = empty and isin = isin and insert = insert and delete = delete
 and inorder = inorder and inv = rbt
 proof (standard, goal_cases)
   case 1 show ?case by (simp add: empty_def)
 next