make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
theory Hoare_Parallel
imports OG_Examples Gar_Coll Mul_Gar_Coll RG_Examples
begin
end