moved MaSh into own files

distinguish updates and queries + cleanups

don't ask E to generate a detailed proofs if not needed

tuning

gracefully compute cardinality of sets (to avoid type protectors)

better tautology elimination

generate lambdas and skolems again

tuning

generate deep terms as feature

generate theory name as a feature

adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)

merged

adding the hotel key card example in Quickcheck-Examples

adding a missing entry to predicate compiler's setup

compile

tuning

cleanup

more precise dependencies -- eliminate tautologies

generate problem file

improve feature list generation

cleaner accessibility file

first go at generating files for MaSh (machine-learning Sledgehammer)

abandoned import of isatest reports into (old version of) mira -- unstable, and not worth the maintenance effort

make sure var/running dir exists for isatest

removed switched-off atbroy102 from isatest; no cygwin test currently running, needs a working server somewhere

prefer lxbroy[23] as standard test machines;

discontinued XSYMBOL_INSTALLFONTS (cf. 40fab092d2a2);

discontinued odd XSYMBOL_INSTALLFONTS, which is private to PG-3.7.x (isafonts.informatik.tu-muenchen.de:7200 no longer exists);

tuned;

discontinued obsolete attribute "COMP";