added remdups_filter lemma

merged

subst_signatures

tuned

exported build_tsig

crude support for type aliasses and corresponding constant signatures

generalized some lemmas

added Crude_Executable_Set.thy

read_dimacs_cnf_file can now read DIMACS files that contain successive white-space characters.

Expand nested abbreviations before applying dummy patterns.

Removed eq_to_mono2, added not_mono.

Streamlined setup for monotonicity rules (no longer requires classical rules).

Simplified treatment of monotonicity rules.

removed obsolete test tags;

Added tag Isabelle2009-1 for changeset 6a973bd43949

slightly less ambitious settings, to avoid potential out-of-memory problem;

even higher proof-shell-quit-timeout -- saving main HOL takes 20s on a *fast* machine;

updated date;

more robust treatment of spaces in directory names;

adding subsection about the predicate compiler to the code generator tutorial

Added tag isa2009-1-test for changeset e1c262952b02

updated date;

Expand nested abbreviations before applying dummy patterns.

raised proof-shell-quit-timeout to accomodate bulky write-back images;

deactivated default for E_HOME, SPASS_HOME -- now configured as components; deactivated default for VAMPIRE_HOME -- superceded by remote_vampire;

double check file permissions of write-back image -- more robust for root or administrator on Cygwin;

tuned message;

added HOLCF image;