clarified store.clean_output: cleanup user_output_dir even in system_mode;

clarified store directories; discontinued settings ISABELLE_PATH, ISABELLE_OUTPUT;

tuned;

clarified handling of output heap;

tuned;

added lemmas

more abstract database access;

tuned;

clarified heap vs. database operations: discontinued correlation of directory;

tuned;

tuned signature;

support Store with options;

more exports;

updated some Sledgehammer components, following Makarius advice

export more theory and session structure;

tuned signature;

clarified signature;

read theory content from session database;

clarified signature;

misc tuning and clarification;

NEWS and CONTRIBUTORS for 8b50f29a1992

proper PIDE positions;

avoid race condition wrt. ISABELLE_TMP, which is removed in Bash.cleanup() before Bash.result(progress_stdout);

clarified "consolidation" vs. "presentation";

tuned signature;

merged

tuned;

more thorough checks for theory name consistency (for extend, not just merge);

more uniform output (cf. 450cefec7c11);

removed duplicates

added lemmas

tuned headers;

move FuncSet back to HOL-Library (amending 493b818e8e10)

merged

cleaning up sorted

merged

support for dynamic document output while editing;

adjust position according to offset of command/exec id;

tuned signature (see Command.eval_state);

export generated document.tex, unless explicit document=false;

more general presentation hook, with document preparation as application;

clarified signature: more explicit type "context" with full options;

more explicit type Thy_Output.segment;

clarified signature; more operations;

more sorted cleaning

cleaning up sorted

merged

more uniform types vs. consts;

more concise information;

export foundational theory content in Scala;

clarified markup;

tuned signature;

tuned -- use XZ.Cache;

clarified implicit compression;

tuned -- use XZ.Cache;

more exports; misc tuning and clarification;

tuned;

more operations;

tuned

tuned

mv lemma

removed unused lemma

tuned

removed some non-essential rules

added lemmas

new tool Code_Lazy

some export of foundational theory content;

support for general theory presentation;

guard result exports via export_pattern -- avoid bombing client via huge blobs;

tuned;

clarified output: avoid costly operations on huge blobs;

unused;

more scalable -- avoid huge lines within stdout;

slightly more ambitious parallelism (again);

more scalable API;

proper heading;

removed unused Java FX modules (it will be unbundled from JDK eventually);

tidied some messy proofs

merged

more lemmas

merged

simpler types

auto-tidying

merged

more on infinite products

merged

part tidy-up of Determinants

less ambitious parallelism, notably for threads=2;

more informative error, notably for missing executable;

tuned signature;

clarified future scheduling parameters, with support for parallel_limit;

record total number of tasks;

merged

more infinite product theorems

proper merge of items without term index (amending b969263fcf02);

announce sorted changes

merged

one tiny fix

merged

merged

tidying more messy proofs

merged

more efficient code

merged

command-line tool "isabelle export"; more documentation; tuned;

more efficient query;

more robust: self-export only;

tuned signature;

merged

more "sorted" changes

more "sorted" changes

new def of sorted and sorted_wrt

more operations;

merged

return exports as result for Isabelle server;

more checks;

tuned;

more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure; tuned;

clarified signature; avoid pointless compression;

store exports within PIDE command state; Markup.Export.unapply: proper NAME;

removed some lemma duplicates

typo

more appropriate notion of emptiness

merged

more tidying

starting to tidy up Interval_Integral.thy

more operations;

merged

store exports in session database, with asynchronous / parallel compression;

tuned signature;

tuned signature; clarified modules;

tuned signature;

protocol message for export of theory resources;

hexadecimal representation of byte string;

cleanup session output before starting build job; tuned signature;

reinstated old lemma name

updated to lemma name change

removed asm "finite"

merged

no censorship of view title;

set view title dynamically;

tuned

tuned

Some tidying up (mostly regarding summations from 0)

tidied up Infinite_Products

merged

fixed HOL-Analysis

merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)

added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly

a lemma about infinite products

merged

tidying up and using real induction methods

tuned -- slightly smaller future closure size;

clarified menu actions;

purge history more thoroughly (see also 3156faac30a7);

merged

type class generalisations; some work on infinite products

merged

simplified some messy proofs

clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations); tuned headers;

avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";

merged

more general tidying up

prefer explicit error message to unspecific Options exception: Z3 proof traces may lack information necessary for replay when dealing with quantified formulas

cleaned up more messy proofs

more defer/prefer

getting rid of more "defer", etc.

getting rid of "defer"

another big cleanup

merged

minor typeclass generalisations and junk removal

merged

more messy proofs

merged

new simp modifier: reorient

small typeclass generalisations

merged

some of Jose Divasón's material from Rank_Nullity_Theorem/Miscellaneous

spelling;

more messy proofs redone, and new material

merged

merged

new material on matricies by Tim Makarios (from Tarskis_Geometry in the AFP)

merged

tuned -- avoid spurious exception trace for "the";

proof of concept for residue rings over int using type numerals

more correct error message

uniform tagging for printable and non-printable literals

merged

fixing more messy proofs

more ambitious parallelism (in contrast to a8ee8e4884ec): pri = 1 ensures that internal proof tasks are executed before the already forked theory outline with pri = 0;

eliminated pointless special case (see also a8ee8e4884ec, c4c4c2f01723);