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;