src/HOL/Data_Structures/RBT_Set.thy
changeset 68440 6826718f732d
parent 68431 b294e095f64c
child 68998 818898556504
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Wed Jun 13 11:53:25 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Wed Jun 13 15:24:20 2018 +0200
     1.3 @@ -256,7 +256,7 @@
     1.4  
     1.5  text \<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 = rbt
    1.11  proof (standard, goal_cases)