more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;

merged

command 'print_term_bindings' supersedes 'print_binds';

Proof General legacy;

removed obsolete "isabelle unsymbolize";

minor renovation of slightly odd and old README;

sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;

tweaking

correctly take weights into consideration

tuned whitespace and parentheses

use right theory name for theorems in evaluation driver

killed dead code

reintroduced 'extra features' + only print message in verbose mode

got rid of hard-coded weights, now that we have TFIDF

tuning

tuning

reintroduced 'extra features' but with lower weight than before (to account for tfidf)

resolution modulo double negation

compile

merged two small theory files

tuned variable names

whitespace tuning

repaired BNF 'size' generation tactic for datatypes mixng old- and new-style datatypes on the right-hand side

tiny refinements

suppress documentation "how_to_prove_it" for now, notably for release;

updated to jdk-7u60 -- back to stable Java 7 for Isabelle2014 release;

updated generated file;

merged

updated cygwin on server; include unzip, which is required for src/Doc/JEdit;

tuning