allow explicit specification of additional session directories;

more errors;

some HOL sessions;

cumulate semantic Session_Info, based on syntactic Session_Entry; tuned errors;

more tight treatment of reset_name;

more informative errors;

added parser for Session_Info;

repair MaSh exporter

optimize parent computation in MaSh + remove temporary files

make the monomorphizer more predictable by making the cutoff independent on the number of facts

speed up MaSh queries

use better score function, based on previous evaluation (cf. Deduct 2011 slides)

attempt at meshing according to more meaningful factors

don't include hidden facts in relevance filter + tweak MaSh learning

removed debugging output

removed expensive HO check in MaSh

speed up tautology/metaness check

optimized MaSh output by chunking it

fixed MaSh state load code so it works even if the facts are read in disorder

learn from minimized ATP proofs

improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)

use async manager to manage MaSh learners to make sure they get killed cleanly

more consolidation of MaSh code

removed lie

drastic overhaul of MaSh data structures + fixed a few performance issues

fixed order of accessibles + other tweaks to MaSh

added option to control which fact filter is used

mesh facts by taking into consideration whether a fact is known to MeSh

implemented meshing of Iter and MaSh results

implemented MaSh QUERY operation

refactored MaSh ADD code so it can be used for SUGGEST as well

implemented low-level MaSh ADD operation

make tracing an option

cleaner handling of metacharacters + freshness of one-off facts

better zipping of MaSh facts

implemented MaSh learn theory function

more work on MaSh

improved MaSh string escaping and make more operations string-based

more implementation work on MaSh

started implementing MaSh client-side I/O

tweak output

centrally construct expensive data structures

more work on MaSh

compile

gracefully handle the case of empty theories when going up the accessibility chain

tuning

doc updates

renamed Sledgehammer options

more code rationalization in relevance filter

moved override out of iter filter

fixed bug introduced when moving code around

systematize lazy names in relevance filter

rationalize relevance filter, slowing moving code from Iter to MaSh

killed one file

dependency tuning

renaming

clean up dependencies

explicitly import Dlist theory into library

tuned whitespace

dropped ancient example generates

basic support for session ROOT files, with examples for FOL and ZF;

more accurate imitation of formal text;

avoid Source.fromFile, which does not necessarily close its input;

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