src/HOL/Data_Structures/Tree_Set.thy
changeset 68440 6826718f732d
parent 68431 b294e095f64c
     1.1 --- a/src/HOL/Data_Structures/Tree_Set.thy	Wed Jun 13 11:53:25 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Wed Jun 13 15:24:20 2018 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4    "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
     1.5  by(induction t) (auto simp: del_list_simps split_minD split: prod.splits)
     1.6  
     1.7 -interpretation Set_by_Ordered
     1.8 +interpretation S: Set_by_Ordered
     1.9  where empty = empty and isin = isin and insert = insert and delete = delete
    1.10  and inorder = inorder and inv = "\<lambda>_. True"
    1.11  proof (standard, goal_cases)