recovered Options.default_markup, e.g. for src/Doc/antiquote_setup.ML (amending 16519cd83ed4);

tuned;

clarified signature;

clarified signature;

dedicated case option for code generation to Scala

minor performance tuning, notably for Library.fold_string etc.;

clarified file name;

purge log files -- avoid old errors;

expose bibtex errors;

proper exception;

proper \isakeeptag (amending 13b5c3ff1954);

tuned;

NEWS;

merged

purge more carefully (amending 26f548370e8d); recovered 'display_drafts';

more error information according to @<Print type of token list@> in pdfweb.tex;

avoid redundant positions;

positions as postlude: avoid intrusion of odd %-forms into main tex source;

scan only one line, for more detailed positions;

purge more thoroughly;

option document_positions;

clarified file pattern;

ensure separation of TeX tokens;

simplified positions -- line is also human-readable in generated .tex file;

tuned message;

avoid excessive whitespace between antiquotations and text;

updated documentation;

more robust range on preceding comment-line; no range for blank lines; avoid recursive output_text/mark_range; clarified Latex.output_token (no range) vs. Thy_Output.present_token (with range);

proper file;

clarified file positions;

more operations;

tuned messages;

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;