| changeset 62390 | 842917225d56 | 
| parent 61790 | 0494964bb226 | 
| child 63411 | e051eea34990 | 
--- a/src/HOL/Data_Structures/Lookup2.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Data_Structures/Lookup2.thy Tue Feb 23 16:25:08 2016 +0100 @@ -18,4 +18,4 @@ "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x" by(induction t) (auto simp: map_of_simps split: option.split) -end \ No newline at end of file +end