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

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

tuned proofs -- eliminated old-fashioned COMP and rev_contrapos;

prefer sys.env from scala 2.9;

prefer sys.exit from scala 2.9;

internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;

more explicit directory structure Admin/Release/; updated to Admin/components;

merged

Stub theory for division on functionals.

slightly modernized ISABELLE_GHC etc. -- /usr/bin is more likely to provide it by default (notably on macbroy2[0-9] and lxbroy*);

more precise cover

don't generate any type class axioms for free types for monomorphic encodings

update docs

tuning

prefer hook in Admin/ to initialize components

corrected: avoid shadowing of variable

merged

adding some minimal documentation and an example of quickcheck's interfaces

exporting important function for the "many conjecture refutation" compilation of quickcheck

merged

new type class for computing finiteness of types with instantiations