isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

clarified topological ordering: preserve order of adjacency via reverse fold;
2012-07-19, by wenzelm
support Session.Queue with ordering and dependencies;
2012-07-19, by wenzelm
clarified signature;
2012-07-19, by wenzelm
more explicit treatment of initial Pure sessions;
2012-07-19, by wenzelm
more general support for Isabelle/Scala command line tools;
2012-07-19, by wenzelm
tuned width;
2012-07-19, by wenzelm
prefer general Properties.Value.Boolean;
2012-07-19, by wenzelm
more SHA1.digest operations;
2012-07-18, by wenzelm
tuned import;
2012-07-18, by wenzelm
tuned source structure;
2012-07-18, by wenzelm
allow explicit specification of additional session directories;
2012-07-18, by wenzelm
more errors;
2012-07-18, by wenzelm
some HOL sessions;
2012-07-18, by wenzelm
cumulate semantic Session_Info, based on syntactic Session_Entry;
2012-07-18, by wenzelm
more tight treatment of reset_name;
2012-07-18, by wenzelm
more informative errors;
2012-07-18, by wenzelm
added parser for Session_Info;
2012-07-18, by wenzelm
repair MaSh exporter
2012-07-18, by blanchet
optimize parent computation in MaSh + remove temporary files
2012-07-18, by blanchet
make the monomorphizer more predictable by making the cutoff independent on the number of facts
2012-07-18, by blanchet
speed up MaSh queries
2012-07-18, by blanchet
use better score function, based on previous evaluation (cf. Deduct 2011 slides)
2012-07-18, by blanchet
attempt at meshing according to more meaningful factors
2012-07-18, by blanchet
don't include hidden facts in relevance filter + tweak MaSh learning
2012-07-18, by blanchet
removed debugging output
2012-07-18, by blanchet
removed expensive HO check in MaSh
2012-07-18, by blanchet
speed up tautology/metaness check
2012-07-18, by blanchet
optimized MaSh output by chunking it
2012-07-18, by blanchet
fixed MaSh state load code so it works even if the facts are read in disorder
2012-07-18, by blanchet
learn from minimized ATP proofs
2012-07-18, by blanchet
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
2012-07-18, by blanchet
use async manager to manage MaSh learners to make sure they get killed cleanly
2012-07-18, by blanchet
more consolidation of MaSh code
2012-07-18, by blanchet
removed lie
2012-07-18, by blanchet
drastic overhaul of MaSh data structures + fixed a few performance issues
2012-07-18, by blanchet
fixed order of accessibles + other tweaks to MaSh
2012-07-18, by blanchet
added option to control which fact filter is used
2012-07-18, by blanchet
mesh facts by taking into consideration whether a fact is known to MeSh
2012-07-18, by blanchet
implemented meshing of Iter and MaSh results
2012-07-18, by blanchet
implemented MaSh QUERY operation
2012-07-18, by blanchet
refactored MaSh ADD code so it can be used for SUGGEST as well
2012-07-18, by blanchet
implemented low-level MaSh ADD operation
2012-07-18, by blanchet
make tracing an option
2012-07-18, by blanchet
cleaner handling of metacharacters + freshness of one-off facts
2012-07-18, by blanchet
better zipping of MaSh facts
2012-07-18, by blanchet
implemented MaSh learn theory function
2012-07-18, by blanchet
more work on MaSh
2012-07-18, by blanchet
improved MaSh string escaping and make more operations string-based
2012-07-18, by blanchet
more implementation work on MaSh
2012-07-18, by blanchet
started implementing MaSh client-side I/O
2012-07-18, by blanchet
tweak output
2012-07-18, by blanchet
centrally construct expensive data structures
2012-07-18, by blanchet
more work on MaSh
2012-07-18, by blanchet
compile
2012-07-18, by blanchet
gracefully handle the case of empty theories when going up the accessibility chain
2012-07-18, by blanchet
tuning
2012-07-18, by blanchet
doc updates
2012-07-18, by blanchet
renamed Sledgehammer options
2012-07-18, by blanchet
more code rationalization in relevance filter
2012-07-18, by blanchet
moved override out of iter filter
2012-07-18, by blanchet
fixed bug introduced when moving code around
2012-07-18, by blanchet
systematize lazy names in relevance filter
2012-07-18, by blanchet
rationalize relevance filter, slowing moving code from Iter to MaSh
2012-07-18, by blanchet
killed one file
2012-07-18, by blanchet
dependency tuning
2012-07-18, by blanchet
renaming
2012-07-18, by blanchet
clean up dependencies
2012-07-18, by blanchet
explicitly import Dlist theory into library
2012-07-17, by haftmann
tuned whitespace
2012-07-17, by haftmann
dropped ancient example generates
2012-07-17, by haftmann
basic support for session ROOT files, with examples for FOL and ZF;
2012-07-17, by wenzelm
more accurate imitation of formal text;
2012-07-17, by wenzelm
avoid Source.fromFile, which does not necessarily close its input;
2012-07-17, by wenzelm
tuned imports;
2012-07-17, by wenzelm
basic setup for Isabelle build tool;
2012-07-17, by wenzelm
more standard main method;
2012-07-17, by wenzelm
avoid slightly odd share_common_data -- Poly/ML 5.5.x should manage low-memory situations (cf. f55e77f623ab);
2012-07-17, by wenzelm
improved equality optimisation in Quickcheck
2012-07-17, by bulwahn
more direct Sorts.has_instance;
2012-07-16, by wenzelm
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
2012-07-16, by wenzelm
comment;
2012-07-16, by wenzelm
added universal jdk-6u31.tar.gz component (post Isabelle2012);
2012-07-16, by wenzelm
more components from Isabelle2011-1 and Isabelle2012;
2012-07-16, by wenzelm
deactivate Find_Unused_Assms_Examples to see if isabelle test's failures is caused by this example file
2012-07-16, by bulwahn
merged;
2012-07-15, by wenzelm
updated versions
2012-07-15, by krauss
added component integrity checks and some initial checksums
2012-07-15, by krauss
prefer canonical fold_rev;
2012-07-15, by wenzelm
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);
2012-07-15, by wenzelm
tuned proof;
2012-07-15, by wenzelm
more precise imports;
2012-07-15, by wenzelm
removed some old/unused stuff;
2012-07-14, by wenzelm
actually remove former atbroy102/cygwin stuff (cf. 6301046146b6, 08cb859c53cd);
2012-07-14, by wenzelm
more user aliases;
2012-07-14, by wenzelm
removed superfluous lemmas
2012-07-14, by nipkow
fixed typo
2012-07-13, by bulwahn
renaming the example file which was overlooked before
2012-07-13, by bulwahn
a first guess to avoid the Codegenerator_Test to loop infinitely
2012-07-12, by bulwahn
get attachments sent even on lxbroy Gentoo machines
2012-07-12, by Gerwin Klein
moved most of MaSh exporter code to Sledgehammer
2012-07-11, by blanchet
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
2012-07-11, by blanchet
dummy implementation
2012-07-11, by blanchet
split relevance filter code into three files
2012-07-11, by blanchet
optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code
2012-07-11, by blanchet
add Isabelle dependencies to tweak relevance filter
2012-07-11, by blanchet
generate ATP dependencies
2012-07-11, by blanchet
merged
2012-07-11, by bulwahn
adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
2012-07-11, by bulwahn
comment
2012-07-11, by blanchet
nicer output
2012-07-11, by blanchet
rationalized output
2012-07-11, by blanchet
generate Meng--Paulson facts for evaluation purposes
2012-07-10, by blanchet
tuning
2012-07-10, by blanchet
export useful functions
2012-07-10, by blanchet
instantiate induction rules
2012-07-10, by blanchet
MaSh evaluation driver
2012-07-10, by blanchet
moved MaSh into own files
2012-07-10, by blanchet
distinguish updates and queries + cleanups
2012-07-10, by blanchet
don't ask E to generate a detailed proofs if not needed
2012-07-10, by blanchet
tuning
2012-07-10, by blanchet