more careful witness' type analysis

removed outdated example

remove unused code

remove Eisbach's dependency on HOL

match method now makes proper use of context_tactic

merged

nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.

added AA_Map; tuned titles

tuned

Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.

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;