--- a/src/HOL/Library/RBT_Mapping.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Library/RBT_Mapping.thy Tue Feb 23 16:25:08 2016 +0100 @@ -206,4 +206,4 @@ \vspace{1ex} \<close> -end \ No newline at end of file +end