| changeset 61588 | 1d2907d0ed73 |
| parent 61581 | 00d9682e8dd7 |
| child 61640 | 44c9198f210c |
--- a/src/HOL/Data_Structures/Tree_Set.thy Thu Nov 05 11:59:45 2015 +0100 +++ b/src/HOL/Data_Structures/Tree_Set.thy Thu Nov 05 18:38:08 2015 +0100 @@ -61,7 +61,7 @@ interpretation Set_by_Ordered where empty = Leaf and isin = isin and insert = insert and delete = delete -and inorder = inorder and wf = "\<lambda>_. True" +and inorder = inorder and inv = "\<lambda>_. True" proof (standard, goal_cases) case 1 show ?case by simp next