separate image for prerequisites of codegen tutorial

modernized cartouches

even more pervasive replacement of auxiliary destination

merged

more detailed runtime statistics for Z3 proof reconstruction

merged

proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);

updated to scala-2.11.5;

refrain from default task_context for all protocol commands, e.g. relevant for "build_theories" to admit Session.shutdown;

more informative build_theories_result: cumulative Runtime.exn_message;

tuned;

more type-safe handler interface; proper progress for Build.Handler;

clarified build_theories: proper protocol handler;

added Promise.cancel;

clarified build_theories;

added Path.decode in ML, in correspondence to Path.encode in Scala;

some support for PIDE batch session; clarified Thy_Info.use_thys_options and corresponding protocol command;

piecewise measurability using restrict_space; cleanup Borel_Space

tuned

indent broken lines of bindings in do blocks

more line breaks in integral notation

allow line breaks in integral notation

allow line breaks in probability syntax

don't minimize chained facts -- this leads to subtle failures, e.g. if a method succeeds without a chained fact but fails with it

NEWS

measurability prover: removed app splitting, replaced by more powerful destruction rules

tuned warnings: observe Context_Position.is_visible;

removed unused/non-portable with_tmp_fifo;

discontinued fifo channel, always use portable socket;

tuned -- more Sidekick-friendly layout;

do not crash into already running exec, instead join its lazy result in the subsequent step (amending 59f1591a11cb);

more explicit errors;

proper latex;

tuned -- less redundant;

proper Session.save with shutdown, which is relevant to avoid persistent threads;

tuned latex;

merged

always use socket to test performance and stability;

explicit shutdown of scheduler and worker thread farm, assuming Session.shutdown() before saving heap image; discontinued spontaneous thread expiration from TTY age to avoid sporadic Simple_Thread.fork, which is potentially fragile in situations of resource shortage;

tuned;

discontinued worker_trend: prefer constant number of active + reserve threads; tuned exceptional situations;

tuned;

added lemma

typo

avoid writing into source

clarified active_job: take dependencies into account (e.g. future based on promise);

tuned;

non-strict print_state: display old proof state on failure, e.g. unfinished command;

permissive worker_start: failure to fork thread is deferred to later attempt to provide missing threads, without crashing scheduler;

clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish; discontinued spontaneous thread expiration from TTY age to avoid sporadic Simple_Thread.fork, which is potentially fragile in situations of resource shortage;

ignore print process even after fork, to avoid loosing active worker threads;

rel_pmf OO: conversion to nat is not necessary

merged

simplify construction for distribution of rel_pmf over op OO

prefer option for default code printing width

modernized and more uniform style