src/HOL/Data_Structures/Tree_Map.thy
changeset 61790 0494964bb226
parent 61686 e6784939d645
child 63411 e051eea34990
     1.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Sat Dec 05 16:13:28 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Sat Dec 05 16:33:20 2015 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4  
     1.5  subsection "Functional Correctness Proofs"
     1.6  
     1.7 -lemma lookup_eq:
     1.8 +lemma lookup_map_of:
     1.9    "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
    1.10  by (induction t) (auto simp: map_of_simps split: option.split)
    1.11  
    1.12 @@ -48,7 +48,7 @@
    1.13  proof (standard, goal_cases)
    1.14    case 1 show ?case by simp
    1.15  next
    1.16 -  case 2 thus ?case by(simp add: lookup_eq)
    1.17 +  case 2 thus ?case by(simp add: lookup_map_of)
    1.18  next
    1.19    case 3 thus ?case by(simp add: inorder_update)
    1.20  next