remember ATP flops to avoid repeating them too quickly

remember which MaSh proofs were found using ATPs

rule out same "technical" theories for MePo as for MaSh

don't generate queries for empty dependencies

crank up max number of dependencies

never use MaSh in Metis examples, to avoid one dimension of nondeterminism

merged

more informative process exit code;

timeout for session build job; tuned error messages;

static outer syntax based on session specifications;

declare trE and tr_induct as default cases and induct rules for type tr

reject path variable nesting explicitly;

simplified custom document/build script, instead of old-style document/IsaMakefile;

cleaner temporary file cleanup for MaSh, based on tried-and-trusted code

merged

don't tag negatively naked variables

support older versions of Vampire

document E-MaLeS

added E-MaLeS to list of provers for testing

discontinued unused etc/sessions catalog;

allow session specifications in arbitrary order;

tuned;

report commands as formal entities, with def/ref positions;

more official command specifications, including source position;

more antiquotations;

declare keywords only once;

more antiquotations;

more antiquotations;

more standard bootstrapping of Pure outer syntax;

fixed document;

store parent heap stamp as well -- needs to be propagated through the build hierarchy; misc tuning;

more standard bootstrapping of Pure.thy;

more precise guide for bibtex/makeindex -- dummy files should be sufficient;

added offline test for skip_proofs;

clarified ISABELLE_FULL_TEST;

explicit option skip_proofs;

recovered comination of Toplevel.skip_proofs and Goal.parallel_proofs from 9679bab23f93 (NB: skip_proofs leads to failure of Toplevel.proof_of);

removed junk;

no longer force STIX fonts onto the user -- NB: STIXv1.0.0 is outdated and Mac OS 10.7 ships its own copy of STIX already;

more prominent file name;

updated isatest settings for isabelle build;

more portable hex_nibble: avoid disagreement of Poly/ML and SML/NJ on StringCvt.HEX;

merged

print full path;

Remove Lift_RBT.thy, it's in HOL/Library/RBT.thy now

add testing file for RBT_Set

implementation of sets by RBT trees for the code generator

use lifting/transfer formalization of RBT from Lift_RBT

a couple of additions to RBT formalization to allow us to implement RBT_Set

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;