src/HOL/Data_Structures/Lookup2.thy
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