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