add filterlim rules for exp and ln to infinity

add filterlim rules for inverse and at_infinity

add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image

add filterlim rules for unary minus and inverse

rename filter_lim to filterlim to be consistent with filtermap

add check to Cooper's algorithm that left-hand of dvd is a numeral

merged

robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer

avoid odd warnings due to failure of systray icon;

synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic); clarified signature -- cache init is unsynchronized and hopefully used at most once per file;

tuned;

recovered error to finish proof (e.g. bad obtain export) from 223f18cfbb32; tuned message;

semi-automated Cygwin setup;

misc tuning;

updated to sumatra_pdf-2.1.1;

tuned order of functions

proper quoting of paths in MaSh

updated to jedit_build-20121201 (based on jedit-5.0.0);

moved isabelle shortcuts to main jEdit.props, in order to have them migrated to the "imported" keymap;

leave ALTERNATIVE_DISPATCHER mostly enabled on Mac OS X, to get events for COMMAND/Meta combinations, which seem to produce only KEY_PRESSED in Java 7, not KEY_TYPED as in Java 6;

updated to jedit-5.0.0;

more generic directory name to facilitate tracking changes of diffs;

merged

tuned

added 'print_inductives' command;

print formal entities with markup;

tuned labels;

renamed dockable "Prover Session" to "Theories"; more uniform Library.lowercase/uppercase;

tuned import;

alternative shortcut for English keyboard;

merged

eliminated redundant is_ident -- more official is_identifier;

updated to jdk-7u9;

updated to exec_process-1.0.3;

report proper pid *after* fork;

prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;

more defensive retry via fork;

merged

parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned

simplified use of fold/map; tuned;

tuned;

prefer 32 bit platform for ISABELLE_FULL_TEST, to make memory problems more explicit instead of disk thrashing (notably in HOL-Quickcheck_Benchmark);

merged

make SML/NJ happy (give names for all fields in a record)

more robust syntax that survives collapse of \<^isub> and \<^sub>;

further update and clarification of the all-important README_REPOSITORY;

more uniform ML statistics;

merged

improved readability

tweaked calculation of sledgehammer messages

adapted sledgehammer warnings

fixed case split preplaying

fixed preplaying of case splits; incorperated new name of structure: Isabelle_Markup -> Markup

preplay case splits

added warning when shrinking proof without preplaying

deal with the case that metis does not time out, but fails instead