src/HOL/Data_Structures/Tree23_Set.thy
changeset 68440 6826718f732d
parent 68431 b294e095f64c
child 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Wed Jun 13 11:53:25 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Wed Jun 13 15:24:20 2018 +0200
     1.3 @@ -379,7 +379,7 @@
     1.4  
     1.5  subsection \<open>Overall Correctness\<close>
     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 = bal
    1.11  proof (standard, goal_cases)