--- a/src/HOL/Library/Discrete.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Library/Discrete.thy Tue Feb 23 16:25:08 2016 +0100 @@ -219,4 +219,4 @@ end -end \ No newline at end of file +end