diff -r 2b3772ecfdec -r e6784939d645 src/HOL/Data_Structures/Tree23_Map.thy --- 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