| changeset 68440 | 6826718f732d |
| parent 68431 | b294e095f64c |
| child 68998 | 818898556504 |
--- a/src/HOL/Data_Structures/RBT_Set.thy Wed Jun 13 11:53:25 2018 +0200 +++ b/src/HOL/Data_Structures/RBT_Set.thy Wed Jun 13 15:24:20 2018 +0200 @@ -256,7 +256,7 @@ 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)