tuned op

HOL-Analysis: add set_integrable_restrict_space

more correct parentheses

more tight HTML output: avoid extra lines within <pre>;

HTML output for Markdown elements; clarified HTML operations;

updated NEWS

removed dead code

removed old 'add_datatype' ML functions

kill old size infrastructure

repaired whitespace accident from 2505cabfc515

proper namespace for evaluators

tuned

more correct name resolving

skip abstract constructors silently in datatype clauses of computations

removed para about 'old_datatype' in docs

old_datatype no longer exists (cf. 706b1cf7b76d);

merged

PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);

clarified terminology of "markdown_bullet";

compile

updated dependencies + compile

moved 'realizers' into their own theory, now that they are decupled from the old datatype construction

removed 'old_datatype' command

don't test 'old_datatype', which is on its way out

ported inductive realizer to new datatype package

removed needless theorems

store high-level 'size' equations

avoid call to function that may throw an exception in error message

misc tuning and modernization;

more completion templates;

proper purge of auxiliary bibtex theory;

tuned signature;

tuned;

Restored correct spacing for set comprehensions

less redundant;

more robust hyphen (see also "Soft hyphen (SHY) – a hard problem?" http://jkorpela.fi/shy.html);

more robust treatment of conflicts with existing Unicode text;

tuned whitespace;

no check for bibtex entries from other sessions;

clarified signature;

more accurate message patterns;

prefer formal citations; more accurate bibtex entries;

proper bibtex entries;

formal check of @{cite} bibtex entries -- only in batch-mode session builds;

clarified check, notably for bibtex theory (amending 5f082b1fa9fa);

NEWS;

proper check for imports, not just ROOT entries;

tuned signature;

implicit thy_load context for bibtex files (VSCode);

bibtex theory is always required and thus eventually consolidated;

implicit thy_load context for bibtex files;

clarified signature: prefer Document.Node.Name.is_bibtex;

avoid spurious noise: Prover IDE is meant to check for errors;

clarified signature;

avoid clash with special files in HTML output;

unused;

tuned signature;

prefer existing Resources.check_path;

more accurate bibtex entries;

added command 'bibtex_file' (for PIDE interaction only);

clarified default position for empty message pos;

spelling

Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume

fewer warnings;

clarified positions;

check bibtex database on ML side -- for semantic PIDE editing; tuned signature;

clarified directories;

more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);

check bibtex database: errors and warnings;

more symbols;

Merge

Merge

new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product

more symbols;

tuned;

store full blob source for the sake of markup_to_XML;

PIDE markup for non-theory nodes;

discontinued 'display_drafts' command;

action "isabelle.draft" for plain-text preview;

NEWS;

uniform preview for Isabelle/jEdit and Isabelle/VSCode;

tuned;

clarified URL: unique node name;

clarified signature;

proper title; clarified modules;

HTML rendering of \<^control> as in Isabelle/jEdit;

auto update;

clarified modules;

proper HTML title;

tuned signature;

tuned output;

merged

isabelle.preview presents bibtex database files as well;

clarified signature;

isabelle.preview presents auxiliary text files as well;

tuned signature;

tuned signature;

bibtex HTML output via external tool;

merged

tuned op's

tuned op's

tuned op's

tuned op's

tuned op's

tuned op's

tuned;

Some lemmas on complex numbers and coprimality

merged

tuned op's

tuned op's

tuned op's

tuned op's

tuned op's

updated URL;

isabelle update_cartouches -c -t;

have 'try0' display results faster

a conditional paramitrecity prover

removed debug output

made tactics more robust

tuned;

more markup; multiple error output;

added document antiquotation @{session name}; renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation;

more accurate parse_nat/parse_int: avoid corner cases of Int.fromString (e.g. "1.0");

tuned;

disallow theory name "ROOT";

PIDE markup for session ROOT files;

tuned;

more operations;

tuned;

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;