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;