nicer output

rationalized output

generate Meng--Paulson facts for evaluation purposes

tuning

export useful functions

instantiate induction rules

MaSh evaluation driver

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