tuned imports;

basic setup for Isabelle build tool;

more standard main method;

avoid slightly odd share_common_data -- Poly/ML 5.5.x should manage low-memory situations (cf. f55e77f623ab);

improved equality optimisation in Quickcheck

more direct Sorts.has_instance; tuned Sorts.mg_domain;

replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;

comment;

added universal jdk-6u31.tar.gz component (post Isabelle2012);

more components from Isabelle2011-1 and Isabelle2012;

deactivate Find_Unused_Assms_Examples to see if isabelle test's failures is caused by this example file

merged;

updated versions

added component integrity checks and some initial checksums

prefer canonical fold_rev;

back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);

tuned proof;

more precise imports;

removed some old/unused stuff; tuned whitespace;

actually remove former atbroy102/cygwin stuff (cf. 6301046146b6, 08cb859c53cd);

more user aliases;

removed superfluous lemmas

fixed typo

renaming the example file which was overlooked before

a first guess to avoid the Codegenerator_Test to loop infinitely

get attachments sent even on lxbroy Gentoo machines

moved most of MaSh exporter code to Sledgehammer

further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)

dummy implementation

split relevance filter code into three files

optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code

add Isabelle dependencies to tweak relevance filter

generate ATP dependencies

merged

adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck

comment

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