more relation operations expressed by Finite_Set.fold

more set operations expressed by Finite_Set.fold

moved another larger quickcheck example to Quickcheck_Benchmark

HOL-Probability appears to work with smlnj;

document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;

made SML/NJ happy;

renamed session TLA to HOL-TLA to avoid clash with AFP;

clarified directory content operations (similar to ML version);

regenerate ToyList2/ToyList.thy during raw make *after* session build, to ensure that it is updated sporadically (NB: isabelle build does not support generated sources);

multi-threaded HOL-Tutorial with explicit indication of local options;

removed obsolete IsaMakefile + ROOT.ML setup -- doc-src is managed via isabelle build;

removed some old material (inactive since 2002/2003);

updated isatest to isabelle build, which also includes doc-src sessions;

obsolete;

makedist -D retains doc-src component with its "doc" sessions (relevant for testing);

allow negative int values as well, according to real = int | float;

misc tuning;

discontinued unused isabelle jedit debugger; tuned;

more uniform usage of "isabelle tool";

less verbosity;

proper treatment of eof wrt. proper_input -- allow input of spaces/comments only;

tuned signature;

updated ROOT according to 3defa60a7ae3;

merged

re-activating Quickcheck_Narrowing_Examples in Quickcheck_Examples

added build option -c; tuned;

removed build option -f (cf. a125b8040ada), due to slightly inconvenient behaviour on ancestors;

script for downloading components from central store

added build option -f;

corrected slip

discontinued $ISABELLE_HOME/build (cf. 500c6eb6c6dc);

separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;

added Quickcheck_Benchmark (cf. 1959baa22632);

no apparent need for single-threaded execution;

discontinued obsolete Isabelle/build script;

announce advanced support for Isabelle sessions and build management;

some introduction on sessions;

tuned messages;

tuned;

added generated file;

some description of main build options;

more on "Session ROOT specifications";

some description of isabelle build;

tuned;

isabelle browser is another user interface;

renamed isabelle-root minor mode;

discontinued special treatment of Proof General;

top-down order of user interfaces;

misc tuning;

move exception handlers outside of let block

tuned message;

merged

evaluation: allow multiple code modules

tuned proofs -- avoid odd situations of polymorphic Frees in goal state;

merged

restored narrowing quickcheck after 6efff142bb54

tuned proofs -- avoid odd situations of polymorphic Frees in goal state;

unvarify thm statement stemming from old-style definition, to avoid schematic type variables in subsequent goal;

tuned proofs -- avoid odd situations of polymorphic Frees in goal state;

move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used

replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms

give Nat_Arith simprocs proper name bindings by using simproc_setup

tweaks in preparation for type encoding evaluation

merged

replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones

nicer Nitpick subscript output in jEdit

no_check for @{setting} antiquotations -- empty values are treated as undefined on Cygwin;

proper shell variable;

actually check return code;

include doc-src as component, and thus its sessions defined in ROOT;

tuned signature;

delete other log file;

simplified Path vs. JVM File operations;

tuned;

tuned messages;

fewer options;

tuned signature;

prefer explicit datatype Present.dump_mode;

simplified Session.name;

more precise imitation of usedir wrt. Session.name (cf. 45137257399a);

update docs

extract Z3 unsat cores (for "z3_tptp")

bring implementation of traditional encoding in line with paper

further refinement of current/all_current status, which needs to be propagated through the hierarchy (see also Thy_Info.require_thys);

merged

[1] goes after any attributes

Z3 prints so many warnings that the very informative abnormal termination exception hardly ever gets raised -- better be more aggressive here

detect unknown options again

Sledgehammer already has its own ways of reporting and recovering from crashes in external provers -- no need to additionally print scores of warnings (cf. 4b0daca2bf88)

don't export technical theorems for MaSh

repaired accessibility chains generated by MaSh exporter + tuned one function out

generate fact name in queries again + use ATP dependencies when possible

proper all_current, which regards parent status as well;

more build options;

added session HOL-Tutorial;

recovered chapter on Presenting Theories;

avoid clash of Misc/pairs.thy and Types/Pairs.thy on case-insensible file-system;

proper input;

recovered latex job;

adhoc reordering to prevent implicit side-effects of some theories in Types, Rules, Sets;

more build options;

simplified Tutorial sessions; moved original version of generated .tex sources;

proper arguments for old usedir;

more precise imports;

refined "document_dump_mode": "all", "tex+sty", "tex";

allow spaces in file names;

more files for session Pure;

discontinued slightly odd "browser_info_remote" -- it could point to a completely different version of the Isabelle library;

tuned;

remove old output heaps, to ensure that result is valid wrt. check_stamps; tuned signature;

proper imports;

support session groups; tuned signature;

discontinued slightly odd session order, which did not quite work out;

tuned signature;

avoid clash of Advanced/simp.thy vs. Misc/simp.thy;

tuned signature;

actually check source vs. target stamps, based on information from log files;

tuned;

session specifications for doc-src, excluding TutorialI for now;

updated generated files;

clarified no_document situation;

no hardwired default for Proof General component -- its users can use init_component separately;

rail no longer exists;

some updates on "Building a repository version of Isabelle";

added condition = ISABELLE_POLYML according to no-smlnj targets in IsaMakefile;

more standard session setup for WWW_Find;

read/write dependency information; tuned signature;

more files;

more build options;

merged

moving a first Quickcheck example with many computations into a separate session Quickcheck_Benchmark

moving Quickcheck_Examples back to test to run a minimal test even with the mira testing infrastructure

reactivated HOL-NSA-Examples;

tuned order;

more build options;

tuned error;

more explicit checks during parsing;

more explicit document = false to reduce warnings; tuned;

pass parent_base_name, which is required for Session.init sanity check; tuned message;

more session entries;

modernized imports;

more general notion of user ERROR (cf. 44f56fe01528);

tuned messages;

tuned message;

human-readable I/O error;

more session ROOT files;

tuned messages (cf. isabelle makeall);

tuned message;

actually negate "document" (cf. 7483aa690b4f);

clarified no_build vs. verbose;

clarified "document" again, eliminated redundant "no_document";

clarified build -n (no build);

added "document_dump_only" (cf. negated usedir -C);

more precise propagation of options: build, session, theories;

further imitation of ISABELLE_USEDIR_OPTIONS via options;

observe "condition";

observe "quick_and_dirty";

added "browser_info_remote" (cf. usedir -P);

clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;

timing for whole session;

tuned options;

timing is command line options, not system option;

clarified document options;

pass build options to ML; some imitation of usedir Session.init;

added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);

provide explicit ISABELLE_PLATFORM32 as well; discontinued some obsolete platforms; explicit error for unknown platform;

merged

set_vcs now derives prefix from fully qualified procedure / function name

try droppable application using Platypus functionality -- in contrast to earlier AppHack (cf. 9343d4b7c5bf);

updated to Platypus 4.7;

merged

tuned;

clarified init_component: always liberal; reduced divergence of clone from lib/scripts/getsettings;

added system build mode: produce output in ISABELLE_HOME; determine output location more explicitly;

removed redundant check (cf. a8ed41b6280b);

pass ISABELLE_BROWSER_INFO as explicit argument;

removed some old/unused stuff;

updated smlnj settings;

cap the number of facts returned by MaSh

remove MaSh junk associated with size functions

identified "evil" theories for MaSh -- this is rather ad hoc, but so is MaSh anyway

removed MaSh junk arising from primrec definitions

distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh

tuning

faster "save" operation

include unknown local facts in MaSh

ensure all calls to "mash" program are synchronous

don't relearn old facts in Isar mode

took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks

restrict unqualified imports from Haskell Prelude to a small set of fundamental operations

more correct import

merged

NEWS

library theories for debugging and parallel computing using code generation towards Isabelle/ML

also consider current working directory (cf. 3a5a5a992519)

parallel scheduling of jobs; misc tuning;

tuned;

maintain set of source digests, including relevant parts of session entry;

determine source dependencies, relatively to preloaded theories; tuned signature;

propagate defined options; misc tuning;

disallow quotes in path specifications -- extra paranoia;

save image for inner nodes only; misc tuning and simplification;

some actual build function on ML side; further imitation of "usedir" shell script;

tuned -- no dependency on exit function;

more ML_System operations;

restricting Quickcheck_Examples' root file to one basic theory to see if the system error on isatest still occurs

handling partiality in the case where the equality optimisation is applied

merged

updated File.find_files;

more abstract file system operations in Scala, corresponding to ML version;

eliminated obsolete session_manager.scala;

more explicit java.io.{File => JFile};

tune Mesh filter

faster maximal node computation

honor suggested MaSh weights

use CVC3 and Yices by default if they are available and there are enough cores

relearn ATP proofs

don't store fresh names in fact graph, since these cannot be the parents of any other facts

added MaSh to news

cached ancestor computation

minimal maxes + tuning

learn from SMT proofs when they can be minimized by Metis

clean up interesting constants a bit

convenience

name tuning

learning should honor the fact override and the chained facts

fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully

MaSh docs

added "learn_from_atp" command to MaSh, for patient users

get rid of redundant "xxx_INSTALLED" environment variabl

add versioning to MaSh state + cleanup dead code

eliminated special handling of init case, now that "mash.py" has been optimized to handle sequences of add gracefully

more MaSh docs

mention MaSh in docs

use good old MePo filter for SMT solvers by default, since arithmetic is built-in for them

added locality as a MaSh feature

learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds

learn command in MaSh

added possibility of running external MaSh commands asynchronously

renamed ML structures

renamed ML files

renamed "iter" fact filter to "MePo" (Meng--Paulson)

handle local facts smoothly in MaSh

fixed explosion when computing accessibility

use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)

tuning

merged

further imitation of "usedir" shell script; Pure/build observes build_images option, unlike traditional version; tuned signature;

make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests

export code relatively to master directory

require explicit initialization of options; more explicit Position operations;

tuned signature;

define build_options from command line;

some basic Isabelle options;

basic jEdit mode for Isabelle options;

basic support for stand-alone options with external string representation;

minimal build_job;

restrict to required sessions;

proper commas_quote;

tune;

simplified script to build Isabelle/ML;

added eq_file / copy_file corresponding to File.eq / File.copy in ML;

merged

removed ML module DSeq which was a part of the ancient code generator (cf. 58e33a125f32)

deactivating quickcheck narrowing examples to find out if this causes the system error on the current isatest

support for detached Bash_Job with some control operations;

allow catalog entries to be commented-out;

support external processes with explicit environment;

include COMPONENT/etc/sessions as catalog for more directories, for improved scalability with hundreds of entries (notably AFP); misc tuning and simplification;

less redundant data structures;

clarified topological ordering: preserve order of adjacency via reverse fold;

support Session.Queue with ordering and dependencies;

clarified signature;

more explicit treatment of initial Pure sessions;

more general support for Isabelle/Scala command line tools;

tuned width;

prefer general Properties.Value.Boolean;

more SHA1.digest operations;

tuned import;

tuned source structure;

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