generalized proofs

avoid generating TFF1 or polymorphic DFG constructs in Vampire or SPASS problems for goals containing schematic type variables

tuning

exported ML function

setup code generation for filters as suggested by Florian

merged

filter non-matching prems rather than fail in proof procedure in rare cases; include derived example motivating change and some similar other ones

isar-ref entry for print_record

add more frequently-run test for print_record

print_record NEWS and CONTRIBUTORS

print_record: diagnostic printing of record definitions

misc tuning and modernization;

prune old versions more often, to reduce overall heap requirements;

generate HTML version of NEWS, with proper symbol rendering;

tuned -- according to ML version;

suppress somewhat pointless description (NB: this is displayed in 'print_methods');

merged

tuned syntax;

tuned;

\<struct> loses its rendering and is superseded by \<diamondop>; tuned;

discontinued \<struct> syntax;

tuned whitespace;

tuned;

clarified symbol insertion, depending on buffer encoding;

tuned;

fix code generation for uniformity: uniformity is a non-computable pure data.

add uniform spaces

merged

merged

tuned;