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