changeset 61790 | 0494964bb226 |
parent 61749 | 7f530d7e552d |
child 63411 | e051eea34990 |
--- a/src/HOL/Data_Structures/RBT_Map.thy Sat Dec 05 16:13:28 2015 +0100 +++ b/src/HOL/Data_Structures/RBT_Map.thy Sat Dec 05 16:33:20 2015 +0100 @@ -70,7 +70,7 @@ proof (standard, goal_cases) case 1 show ?case by simp next - case 2 thus ?case by(simp add: lookup_eq) + case 2 thus ?case by(simp add: lookup_map_of) next case 3 thus ?case by(simp add: inorder_update) next