| changeset 61686 | e6784939d645 |
| parent 61640 | 44c9198f210c |
| child 61789 | 9ce1a397410a |
--- a/src/HOL/Data_Structures/Tree23_Map.thy Mon Nov 16 12:37:46 2015 +0100 +++ b/src/HOL/Data_Structures/Tree23_Map.thy Mon Nov 16 13:08:52 2015 +0100 @@ -120,7 +120,7 @@ interpretation T23_Map: Map_by_Ordered where empty = Leaf and lookup = lookup and update = update and delete = delete -and inorder = inorder and wf = bal +and inorder = inorder and inv = bal proof (standard, goal_cases) case 2 thus ?case by(simp add: lookup) next