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";

merged

make SML/NJ happy + tuning

tune type arg handling

tuning

fiddled with "tags_at" a bit -- the only non-tuning part of the change is a slight simplification of the typing axioms

remove needless type arguments to "tags_at" encoding

removed obsolete psbooklet;

more directory structure;

explicit is better than implicit;

removed obsolete rev_contrapos (cf. 1d195de59497);