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;