clean log file on Windows;

avoid println with its extra CR on Windows;

removed obsolete option (see 74a1b722507e);

re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;

removed Emacs legacy;

more robust Windows support;

more explicit latex errors;

some support for LaTeX;

added lemmas

added min_list and arg_min_list

made arg_min_on definition

added lemmas

Moved analysis material from AFP

Some facts on the Mangoldt function

dedicated theory for group closure

clarified error;

removed somewhat pointless warning;

uniform use of original theory;

implicit quick_and_dirty as for Toplevel.begin_proof/Proof.global_skip_proof;

avoid smt proofs in distribution

more robust;

merged

clarified document preparation vs. skip_proofs;

"important" annotations

canonical name

tuned output in isar-ref manual;

obsolete (used to be part of old src/Pure/codegen.ML);

just one session for bulky HOL-Analysis documents;

more default tags;

merged

prefer control symbol antiquotations;

more robust, e.g. when Sidekick produces multi-selection;

prefer control symbol antiquotations;

more embedded cartouche arguments; more uniform LaTeX output for control symbols;

name mangling for Latex macros; tuned signature;

removed (un)important tags again to make latex happy

initial version of Analysis document

tuned

merged

more documentation;

explicit tag for document commands: avoid implicit use of document_tags;

system option for default command tags;

tuned;

tuned signature;

Moved material from AFP to Analysis/Number_Theory

merged

NEWS;

added action to make antiquoted cartouche;

tuned signature;

tuned signature;

added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit;

clarified control style;

font style for literal control symbols, notably for antiquotations;

tuned;

tuned comments;

more lemmas

misc tuning and modernization;

simplified session (again, see 39e29972cb96): WordExamples requires < 1s;

tuned;

misc tuning and modernization;

discontinued old 'def' command;

more simplification rules

overhauling of primes

cleaned up and tuned

generalized more lemmas

tuned output;

more operations;

removed inaccessible blobs from Document.Nodes;

more accurate JSON parsing according to http://seriot.ch/parsing_json.php

purge hidden nodes more thoroughly: is_hidden may become true only later;

proper synchronized Map: this may be used on multiple threads;

bij_betw lemma for prime powers

Existence of a holomorphic logarithm

tuned;

clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform;

clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);

clarified description for mixed Mavericks / El Capitan system;

updated documentation;

prefer formal $POLYML_EXE;

clarified main sessions;

updated to official release of polyml-5.7.1; back to more modest default heap: e.g. relevant for Pure session for ML IDE; more robust POLYML_EXE;

suppress warning;

retain files in Pure.thy, notably $POLYML_EXE;

proper context (as in 'term' command);

proper treatment of multi-line cartouche as rudiment of antiquotation, e.g. relevant for syntax-highlighting in Isabelle/jEdit;

more symbols;

prefer Input.source (via cartouche);

updated documentation: JVM is always 64bit;

more symbols;

clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;

macbroy2 is back, still pretending to be on Mavericks for better comparison of performance;

Mac OS X 10.10 Yosemite is baseline;

generalized more lemmas

tuned

tuned and generalized

tuned

new simp rule

Facts about complex n-th roots

more lemmas

macbroy2 is inactive: system update;

tuned

removed overambitious simp rules from e7e54a0b9197

merged

instantiation char :: full_exhaustive by Andreas Lochbihler

avoid lxbroy7, which is presently inaccessible, but retain its build history in db queries;

slightly faster than Poly/ML 5.7.1 library implementation, notably on 32bit multicore (amending 2288cc39b038)

merged

merged

tuned

removed pointless user_home: no measurable impact;

init Mercurial repository for the generated session files;

more operations;

tuned signature;

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;

ROOT cleanup: empty 'document_files' means there is no document;

eliminated pointless warning (see a35af478aee4): empty 'document_files' means there is no document;

more informative timeout message, notably for build_status;

clarified: adapted to ML version;

proper order of initialization (amending 9953ae603a23);

More topological results overlooked last time

merged