less stateful outer_syntax;

discontinued odd Position.column -- left-over from attempts at PGIP implementation;
Position.offset discriminates postions precisely, now also available for Position.line/line_file;

discontinued special treatment of hard tabulators;

eliminated hard tabs;

merged

standardized String.concat towards implode;

more abstract Thy_Load.load_file/use_file for external theory resources;
prefer Boogie_Loader.parse_b2i on already loaded text, bypassing former File.fold_lines optimization;

comment;

clarified Thy_Load.digest_file -- read ML files only once;

tuned signature;