changeset 61588 | 1d2907d0ed73 |
parent 61581 | 00d9682e8dd7 |
child 61678 | b594e9277be3 |
--- a/src/HOL/Data_Structures/RBT_Set.thy Thu Nov 05 11:59:45 2015 +0100 +++ b/src/HOL/Data_Structures/RBT_Set.thy Thu Nov 05 18:38:08 2015 +0100 @@ -73,7 +73,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