added lemma about 'mult', as suggested by Bertram Felgenhauer

tuned proof

merged

Added tag Isabelle2016-1-RC4 for changeset 49708cffb98d

NEWS for e6a3c55b929b;

embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;

avoid extra space intruding rail diagrams (amending 4854f7ee0987);

explicit option editor_generated_input_delay, which is more aggressive by default;

clarified NEWS concerning Library/Poly_Deriv

made MaSh faster and less likely to hang seemingly forever

delay_first for machine generated editor events: avoid starvation, e.g. when operating on big sessions;

Added tag Isabelle2016-1-RC3 for changeset 51be997d0698

op powr for quickcheck[approximation] (amending 67792e4a5486)

skip over inner syntax for indentation;

tuned whitespace;

tuned;

more on "Indentation";

more on "Formal scopes and semantic selection";

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;