tuned;

misc tuning;

made SML/NJ happier

configurable options;

proper level distance according to number of edges, as in old browser;

clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;

tuned;

merged

NEWS;

rubberband method as in old browser; tuned;

tuned;

tuned signature;

proper translate vertex (cf. 4d985afc0565);

tuned signature;

explict layout graph structure, with dummies and coordinates; explicit metrics for dummy box; tuned signature; misc tuning;

tuned;

docs

docs

docs

tuning

formal pretty bodies for class specifications, accepting additional formal bookkeeping in locale.ML

merged

clarified visualizer parameters; do not show dummies by default;

tuned metrics;

proper bounding box including dummies;

more direct coordinates for dummy;

separate module Metrics; maintain static metrics (with font) and visible_graph via layout;

tuned imports;

apply layout on change of options;

avoid fractional font size;

GUI.imitate_font: more explicit result size, e.g. relevant for caching; some graphview font options: Helvetica family is important for self-contained PDF; tuned;

eliminated print modes: offer new and old graph;

docs

generate [code] only with 'code' plugin enabled

docs

added plugins syntax to prim(co)rec

docs

tuning

docs

documented 'transfer' options to 'prim(co)rec'

tuning

Add plugin to generate transfer theorem for primrec and primcorec

use proper context in function

document 'disc_eq_case'

tuning

generate 'disc_eq_case' for Ctr_Sugars

tuning

remove duplication in tactic

document 'case_distrib'

tuning

generate 'case_distrib' for Ctr_Sugars

more metrics, with integer coordinates for layout; initial coordinates: center x as in old browser; Layout.pendulum/collapse: proper downwards range; distance as in old browser (see spaceBetween); move offset as in old browser; more careful comparison wrt. 0.0 (this is IEEE double, not int);

tuned;

misc tuning;

explicit Layout.Point; tuned signature; tuned;

tuned comments;

tuned;

clarified static full_graph vs. dynamic visible_graph; tuned;

tuned signature;

tuned -- more iterators;

tuned;

clarified fit_to_window: floor scale within window bounds;

tuned;

apply_layout: proper repaint; discontinued dysfunctional keyboard interaction: avoid delicate questions about focus and "standard" key bindings in Isabelle/jEdit;

tuned;

tuned;

tuned;

tuned;

tuned signature;

tuned menu items;

tuned signature;

more formal Graph_Display.Node (with ordering) and Graph_Display.Edge; misc tuning; tuned signature;

more uniform support for graph display in ML/Scala;

recovered tooltip from 6e77ddb1e3fb: non-null default is required as prerequisite;

prefer integer coordinates; tuned painting;

clarified bounding box, similar to old graph browser; default font like old browser; clarified metrics; tuned signature;

tuned headers;

less excessive event handling;

tuned;

clarified mouse wheel: conventional scrolling, not scaling;

clarified metrics, similar to old graph browser;

merged

tuned color;

tuned signature;

tuned signature;

more dynamic visualizer -- re-use jEdit font info;

tuned signature;

tuned signature;

more dynamic visualizer -- re-use Isabelle/jEdit options; clarified iTextField error: like Isabelle/jEdit search field; tuned signature;

more standard GUI layout;

tuned;

tuned imports;

tuned;

tuned imports;

tuned signature;

tuned signature;

tuned signature;

tuned;

tuned whitespace;

merged

updated NEWS

optionally display statistics for Z3 proof reconstruction

avoid more than one data slot per module

limit reconstruction time of Z3 proof steps to be able to detect long-running reconstruction steps

converse graph according to Graph_Display;

eliminated TTY/PG legacy;

clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names); tuned;

tuned;

for graph display, prefer graph data structure over list with dependencies; pragmatic distinction between (historically evolved) "session" nodes and (more abstract) "content" nodes

more explict and generic field names

uniform variable name for presentation graphs, to distinguish from values of type Graph.T

stripped ad-hoc diagnostic facility

update map definition in Prog_Prove for new datatype package

explicit message channel for "legacy", which is nonetheless a variant of "warning";

clarified source location;

added system property isabelle.laf, notably for initial system dialog; let L&F take care of font scaling, e.g. GTK+ for Linux where X11 dpi scaling does not really work;

NEWS;

tuned;

clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;

tuned whitespace;

more toplevel pretty printing;

back to full synchronization (cf. eb3e399f5b9f);

proper sequential version;

eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer); clarified Command.run_process etc.: join running eval, bypass running print; eliminated Command.memo in favour of regular Lazy.lazy; more Lazy.lazy status information;

modernized historic example;

more thorough Lazy.is_finished;

3 old example lemmas by Amine listed in the top 100 theorems

update_cartouches; trimmed whitespace;

memo_fork without locking, to avoid rare deadlock in Event_Timer.request due to execution overrun;

typos

unused;

tuned message;

explicit message channels for "state", "information"; separate state_message_color;

imitate font more carefully: err on smaller size; imitate HTML font, notably for Sidekick where short string is also shown as view status message;

more accurate selection of sessions;

more accurate selection of sessions;

discontinued central critical sections: NAMED_CRITICAL / CRITICAL;

more elementary Multithreading.synchronized;

proper Synchronized.var; more atomic operations;

removed remains from Proof General;

obsolete;

system option "pretty_margin" is superseded by "thy_output_margin";

tuned;

proper Synchronized.var;

separate module Random; proper Synchronized.var;

tuned;

tuned signature;

proper context;

afford more heap;

increase chances of success;

recovered metis proof after 115965966e15 (Odd clash of type variables!?);

proper context;

proper context for "net" tactics; avoid implicit Tactic.build_net -- make its operational behavior explicit in application;

tuned;

afford full test, with slightly improved scheduling order;

more generous timeout, to increase chances of at64-poly;

updated according to eb3e399f5b9f;

just one data slot per program unit; tuned signature;

tuned;

just one data slot per program unit; tuned signature;

more standard configuration options;

tuned;

just one data slot per program unit;

tuned;

more frugal Local_Syntax.init -- maintain idents within context;

proper exception for internal program failure, not user-error;

tuned;

suppress irrelevant timing messages (the majority);

less ambitious settings -- increase chances of success;

peek value without synchronization;

avoid repeated access to global variable (101 times in Complex_Main), which is actually synchronized after e557a9ddee5f;

tuning

unfortunately, there is no general function space in the measurable spaces

correctly apply type substitution before checking for function types

avoid generating selectors with function types -- this produce arity inconsistencies

renamed theory file

merged

Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);

tuned;

tuned;

added Par_List in Scala, in accordance to ML version; system property "isabelle.threads" determines size of Scala thread pool, like system option "threads" for ML; avoid ".par" framework with its hard-wired thread pool, which also has problems with cancellation; tuned;

tuned;

rel_pmf commutes with rel_prod

note more facts (always)

conceal typedef more violently

respect order of deads when retrieving bnfs from the database

merged

more informative gutter content: fall-back on background color, e.g. when line numbers are enabled; non-transparent information_message_color like other message colors; removed unused error1_color;

more examples;

more careful handling of auxiliary environment structure -- allow nested ML evaluation;

more markup for improper situations;

more explicit markup for improper commands; clarified CSS rendering;

tuned;

imitate command markup and rendering of Isabelle/jEdit in HTML output;

tuned signature;

more jEdit colors;

proper alt_string markup (cf. 2ceb05ee0331); more jEdit colors, less PG colors (see bb20fb8a57be);

tuned spelling;

clarified language context, e.g. relevant for symbol completion within cartouches;

tuned signature;

proper railsetup;

move topology on enat to Extended_Real, otherwise Jinja_Threads fails

isatest for Mac OS X Yosemite;

tuned spelling;

expand ML cartouches to Input.source; tuned signature;

merged

some special cases for official SML, to treat Isabelle symbols like raw characters;

tuned comment;

clarified Isabelle/ML strings (refining 72238ea2201c);

tuned signature;

instance bool and enat as topologies

NEWS

allow multiple inheritance of targets

tuned module structure

tuned data structures

tuned target inheritance bookkeeping: ancestry is always fully maintained at current entry using canonical merge; n. b. merging of bidirectional dependencies results in effective join of involved nodes: no termination problem since ancestry is always kept explicitly normalized

tuned

tuned names

eta-expand all search patterns using schematic place holders

revert "better" handling of abbreviation from c61fe520602b

tuned variable names

turn application-specific Pattern.matches_subterm into an application-private function

cleaned up mess

add Poisson and Binomial distribution

add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav

proper GUI_Thread context (cf. 7e0d3da6e6d8);

more examples;

tuned header;

generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces

merged

node-specific keywords, with session base syntax as default;

clarified define_command: send tokens more directly, without requiring keywords in ML;

more robust bundle_name: avoid assumptions about identifier, keywords etc.;

tuned signature;

tuned;

clarified token kind;

added Untyped.method convenience (for *this* class only);

tuned signature -- more explicit types;

more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;

node-specific syntax, with base_syntax as default; clarified Document_Model.init: convergence of editor events towards buffer-specific token marker;