--- a/src/Doc/JEdit/JEdit.thy Wed Jan 10 15:21:49 2018 +0100 +++ b/src/Doc/JEdit/JEdit.thy Wed Jan 10 15:25:09 2018 +0100 @@ -2171,4 +2171,4 @@ which sometimes helps in low-memory situations. \<close> -end \ No newline at end of file +end