proper ssh.bash_path;

more operations;

synchronous use_theories, based on consolidated_state;

clarified modules;

optional session_base, e.g. from existing Sessions.Deps in build.scala;

synchronous session start (similar to isabelle.vscode.Server);

tuned signature (again, see 1a9e2a2bf251);

tuned signature;

simplified: eliminated pointless Thy_Document_Model;

theory nodes are never visible: avoid prints, which are not covered by node_consolidated;

load theories via PIDE document update; theory nodes are always required;

tuned signature;

PIDE resources for theory files;

tuned;

tuned signature;

dedicated definition for coprimality

more induct rules on nat

avoid download of components;

local user_home for improved performance, but only after given changeset for stability of measurement history;

support alternative USER_HOME directory;

clarified settings environment;

tuned signature;

tuned;

more options for "isabelle mkroot"; updated documentation;

adapted to changed ROOT syntax (see 13857f49d215); discontinued pointless option -d: always enabled;

converted to Isabelle/Scala;

replaced raw proof blocks by local lemmas

Replaced Raw Proof Blocks by Local Lemmas

tuned

merged

corrected priority

merged

formal dependency on "poly" executable;

removed obsolete workaround: always use existing IntInf.pow;

strip some trailing spaces to force Pure rebuild after ce6454669360

merged

proper build_selection for clean_build (amending 961285f581e6): e.g. relevant for "isabelle build_doc";

clarified signature (again);

clarified exclusion: operate on completed selection, as last step;

tuned;

tuned signature;

clarifified selection: always wrt. build_graph structure; tuned signature;

tuned;

tuned signature;

more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)

integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)

added FIXMEs

Replaced { } proofs by local lemmas; added Hoare logic with logical variables.

backed out odd "bug fix" 671decd2e627;

more recent polyml-test version; afford more heap by default: all platforms are now 64bit and presumably have sufficient memory;

minimal document model for theory files;

tuned signature;

tuned signature;

more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);

uniform graph restriction: build_graph is more sparse than imports_graph and may yield different results for exclude_session_groups / exclude_sessions (e.g. "isabelle build -a -X main");

updated comments;

updated to scala-2.12.4;

testing NewTestRegisterSave;

superseded by plain_identify;

tolerate odd negative times from old log files (before 1698e9ccef2d);

prefer main entry points of HOL;

tuned signature;

clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;

more robust sorted_entries;

more convenient build_log_history;

tuned;

more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;

polyml-test version based on experimental branch NewTestRegisterSave;

support for libgmp on x86_64-darwin;

avoid slow IntInf.pow in Poly/ML 5.7.1 testing version, e.g. relevant for AFP/Lorenz_C0;

delegate boundary cases to existing IntInf.pow;

plain identify job for Isabelle + AFP, independent of any Isabelle technology;

tuned (non-unique example);

clarified situation of global theory names;

less global theories -- avoid confusion about special cases;

proper deps;

allow unrelated ancestor; clarified error;

tuned;

support alternative ancestor session;

support focus_session, for much faster startup of Isabelle/jEdit; more options for "isabelle jedit";

more timing;

tuned;

init only once (see also c0f776b661fa);

proper merge (amending fb46c031c841);

build faster without heap images for minor imports;

proper order for entries from multiple profiles, notably "AFP";

tuned output;

tuned;

logic_selector refers to raw logic name;

clarified terminology;

tuned signature;

do not store bulky Session.Deps;

avoid duplicate invocation of expensive Sessions.deps on full_sessions; tuned;

added isabelle jedit options -B, -P, clarified -R; misc tuning and clarification;

no heap sharing for empty session (e.g. HOL-ODE);

tuned diagram;

clarified ROOT syntax: 'sessions' and 'theories' are optional, but need to be non-empty;

removed unused option, which is potentially expensive;

allow to augment session context via explicit session infos; more compact required_session interface;

synthesize session with all required theories from other session imports;

clarified signature;

clarified signature;

clarified signature;

clarified signature;

clarified signature: global_theories is always required;

tuned;

tuned signature;

clarified modules;

minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;

more permissive: db could be empty after hard crash;

no censorship (in contrast to 2c828c830ad7);

A few more topological results. And made some slow proofs faster

removed ancient nat-int transfer

added lemma

added 'mlex_iff' lemma and simplified proof

merged

recovered document from 9bfb6978eb80;

NEWS;

obsolete;

tuned;