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