tuned comment;

tuned signature;

clarified module name;

abstract code equation may also be default

proper term_of for iarray

string printing conformant to both (S)ML and Isabelle/ML

Fixed bug in bugfix for function package

Fixed variable naming bug in function package

moved bcontfun from AFP/Ordinary_Differential_Equations

ereal: tuned proofs concerning continuity and suprema

spelling error

NEWS;

removed unused operations;

prefer plain session_graph.pdf over GraphBrowser applet;

complete pattern coverage, e.g. relevant for singleton graph;

discontinued obsolete option "document_graph";

provide session_graph.pdf via Isabelle/Scala;

support for session graph from Scala side;

support for off-line graph output, without GUI thread;

make it independent from GUI thread, e.g. for Graph_File.write;

separate module Graph_File;

tuned comments;

tuned;

more compact message;

proper naming convention;

prefer plain tuples;

tuned message;

tuned;

tuned signature;

tuned;

tuned message;

more direct Output.output; avoid newline in Code_Printer/Pretty.str;

avoid newline in Pretty.str;

merged

generalise lemma

integral of the product of count spaces equals the integral of the count space of the product type

import general thms from Density_Compiler

backout cefeea956989: Graphview *is* required in Pure to replace old browser eventually;

backed out obsolete workaround from ef1edfb36af7

disjunctive bottom and supremum lists

sufficent to have graphview as part of jEdit rather than Pure

option for formally inlined class specifications in hierarchy graph

clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;

updated to jdk-7u76, which appears to be more stable than jdk-8u31 (e.g. crashes jEdit/Console plugin of Mac OS X);

updated jdk-8u31;

generalized sum_diff_distrib to setsum_subtractf_nat

tuned measurability proofs

typo in description

tuned message;

always swap panels, which leads to slightly better GUI layout;

suppress inactive controls (again);

tuned colors;

tuned;

more symmetric layout of main panel; misc tuning;

clarified edge_color;

proper tooltips -- override action toolTip which is empty here;

no document here;

discontinued attempt at alphabetic_order -- selection via regex should be sufficient;

suppress some controls that don't work yet;

proper selection of nodes via regular expression;

obsolete -- full layout takes approx. 100ms;

suppress some controls that don't work yet;

tuned;

misc tuning;

proper scrolling wrt. transform; tuned signature;

clarified main actions and keyboard focus;

tuned signature;

retain uniform background, notably wrt. PDF output and tree panel;

option graphview_swap_panels;

support for tree view on graph nodes; misc tuning;

tuned;

no censorship of L&F;

prefer fractional font metrics, for proper scaling of node size;

tuned metrics;

tuned window size for the sake of Windows L&F;

proper refresh after apply_layout, in order to update preferred size, which is required for scroll pane;

more compact content for tighter graph layout;

more explicit Layout.Info: size and content; allow multi-line vertex label, based on content; misc tuning;

clarified Class.pretty_specification: imitate input source;

merged

more efficient Z3 proof reconstruction for rewrite steps with conjunctions and disjunctions, similar to Old_SMT

added simp lemma

tuned

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