tuned whitespace;

tuned signature;

renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;

proper formatting via Pretty.string_of; tuned;

unused;

tuned;

prune old document versions more frequently, for reduced heap usage;

merged

more explicit Pretty.Tree, like in ML; tuned;

tuned;

clarified underlying datatypes;

tuned;

prefer default focus policy, like Output dockable;

tuned;

tuned signature;

support for blocks with consistent breaks; tuned;

preserve break indentation;

support pretty break indent, like underlying ML systems;

register record functions as 'Spec_Rules'

cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer

removed subsumed dependency

removed dead code

add serialisation for abs on integer to target language operation

add gcd instance for integer and serialisation to target language operations

merged

tuned whitespace;

rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;

tuned signature -- clarified modules;

unused;

unused;