diff -r 29800666e526 -r 842917225d56 src/HOL/Data_Structures/Lookup2.thy --- 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) \ 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