src/HOL/Data_Structures/AA_Set.thy
changeset 68440 6826718f732d
parent 68431 b294e095f64c
child 69505 cc2d676d5395
     1.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Wed Jun 13 11:53:25 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Wed Jun 13 15:24:20 2018 +0200
     1.3 @@ -485,7 +485,7 @@
     1.4    (auto simp: del_list_simps inorder_adjust pre_adj_if_postL pre_adj_if_postR 
     1.5                post_split_max post_delete split_maxD split: prod.splits)
     1.6  
     1.7 -interpretation I: 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 = invar
    1.11  proof (standard, goal_cases)