misc tuning and updates;

more on JVM heap space;

tuned;

more on Isar proof language;

documentation for Isabelle/Scala tools; tuned;

more symbols;

avoid import of Complex_Main into Word library (amending 34b7e2da95f6), e.g. to avoid intrusion of const "ii" into theories without complex numbers;

more cronjob tasks, using Poly/ML repository version from 13-Nov-2016;

optional component setup;

clarified msys root; proper copy_files;

clarified setup: avoid alternative C compiler tools, e.g. from Homebrew or MacPorts;

proper admin tool;

tuned output;

back to regular Isabelle tool (reverting abc34a149690);

tuned;

$HOME/.bashrc provides TZ for *all* processes, resulting in proper date for Build_Log.log_date in remote_build_history via ssh (see also fe8f8f88a1d7);

trim more thoroughly, e.g. trailing \0 seen on some system;

tuned;

build sha1 library;

proper CONFIG_SITE for msys;

clarified platform selection;

more robust Windows platform;

copy libgmp on Linux;

prefer raw Admin tool, without Isabelle settings environment;

clarified command-line;

no backup of generated stuff;

more precise environment (for Windows);

proper shell_path for msys inside cygwin;

support other bash executable (notably for msys on Windows);

proper options; simplified command-line; tuned;

build_polyml in Scala;

clarified File.move: target directory like File.copy;

more logging, to see better when files written;

proper cleanup;

uniform order for options and args;

more robust jedit_auto_resolve: avoid losing events deps_changed() / delay_load.invoke();

tuned comment;

proper option for "build", not "build_history" (cf. 5ca4ac099e94);

tuned;

simplified main proof;

misc tuning and modernization;

recovered Output.writeln for remote build_history (cf. ed8940d6295c), in order to have log files copied and removed;

more uniform path syntax, as in ML (see 5a7c919a4ada);

unused since 15865e0c5598;

added Nunchaku component and tuned Nunchaku integration accordingly

back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;

Added tag Isabelle2016-1-RC2 for changeset 2bf4fdcebd49

more robust multithreading;

documentation of @{undefined} (actually introduced in Isabelle2016);

tuned;

Scala "\u" notation uses hexadecimal, not octal (amending 00a135c0a17f);

HOL-Probability: fix import path in Fin_Map

disable CVC4 statistics, and hence crashes upon user interruptions

back to stable scala-2.11.8;

self_update of components, e.g. for vmnipkow9;

updated to scala-2.12.0;

tuned

more accurate start_line: avoid changing the original command (e.g. 'try', 'sledgehammer');

extra newline as for other tools;

prefer standard_path for bash arg;

ignore interrupts from underlying process, e.g. due to out-of-memory situation in ML_Process (see also build.scala);

proper remote repository source;

clarified setup_repository: even more uniform pull vs. clone (see also e84cba30d7ff);

pull isabelle-release;

Merged natlog2 into Discrete.log

moved IMP/Abs_Int_ITP to AFP/Abs_Int_ITP2012

added lemma

added simp rule

generalized experimental feature slightly

provided more efficient interface

back to stable scala-2.11.8;

updated to scala-2.12.0;

tuned

tuned signature

back to post-release mode -- after fork point;

tuned;

updated to new cronjob;

build_release on lxbroy10 appears to work, including latex and remote_dmg;

misc tuning and modernization;

always expand equalities in the transfer relation in transfer_prover (cf. 0a7c97c76f46)

moved contribution to right release

more explicit pull;

types to sets: initial commit

avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar

adapted Nunchaku integration to keyword renaming

tuned;

merged

Added tag Isabelle2016-1-RC1 for changeset 9ee2480d10b7

a more general relator domain rule for the function type

Haskabelle is presently unmaintained;

tuned;

merged

more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;

avoid multiple PIDE markup due to (potentially infinite) backtracking;

more permissive remote_build_history: failure happens routinely and should not lead error, without saving logs;

more lemmas

updated CVC4 component

tuning

more uniform treatment of codatatype vs. datatype map and rel theorem generation (towards nonuniform codatatypes)

added lemma

tuning

preprocess typedefs and quotients correctly

adapted Nunchaku's input syntax to new design decisions

more informative error (see 6e9c22c494c5);

tuned signature -- more friendly for experimentation;

clarified hg push return code: 1 means "nothing to push";

proper Nunchaku setup to use CVC4 and Kodkod

more specific hardware information: relevant for ultimate Mac OS X version;

just one task to identify Isabelle + AFP repository snapshots and build release; report AFP changeset id on website;

tuned;

Deleted spurious markup

latest Mac OS X versions *are* still supported, but presently without formal reference systems;