clarified sessions/directories;

clarified signature default;

clarified signature default;

more operations for type classes;

setup preprocessing for HOL proofs;

support preprocessing of exported proofs;

early setup of proof preprocessing;

clarified output and input of Typ/Term;

adapted to ML version;

more compact XML;

more compact XML: separate environment for free variables; clarified fold_proof_terms vs. fold_proof_terms_types;

more compact XML;

merged

proper ML names;

clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof;

some treatment of OfClass proofs;

tuned signature;

misc tuning and clarification;

proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps;

clarified oracle_proof;

tuned;

tuned;

tuned;

clarified signature;

tuned signature;

more compact XML representation;

proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);

tuned;

tuned -- more direct ML expressions;

clarified modules;

tuned whitespace;

more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;

unused;

document antiquotations + clarify porting text slightly

updated veriT part of Sledgehammer documentation

added para constrasting 'primrec' and 'fun' -- and removed my middle name

dedicated fact collections for algebraic simplification rules potentially splitting goals

merged

tuned;

misc tuning and clarification;

tuned;

tuned -- allow slightly more expensive atomic proofs;

clarified signature -- some operations to support fully explicit proof terms;

tuned;

tuned;

proper treatment of sorts;

tuned app_types: more direct map_proof_types_same;

tuned;

generalized parsing, for e.g. Leo-III

More theorems about limits, including cancellation simprules

Generalised two results concerning limits from the real numbers to type classes

formally augmented corresponding rules for field_simps

clarified option type;

count document nodes via raw file length;

merged

clarified Load_State / load_limit;

clarified Load_State;

discontinued pointless dump_checkpoint and share_common_data -- superseded by base logic image in Isabelle/MMT;

count nodes uniformly: avoid overloaded session;

clarified signature;

simplified proof

tuned signature;

clarified signature: more options;

clarified signature: read full session requirements;

clarified signature;

tuned signature;

clarified options -- more scalable;

obsolete;

proper replacement for (map_types (K dummyT));

Term_XML.Encode/Decode.term uses Const "typargs";

prefer atomic edits -- potentially more robust;

clarified signature -- potentially more robust;

just one dump_checkpoint Main -- potentially more robust;

more robust: avoid update/interrupt of long-running print_consolidation;

avoid censorship of options, e.g. relevant for Isabelle/MMT to provide its own value;

consolidate less aggressively: avoid live-lock when PIDE round-trip takes too long (e.g. in complex theory hierarchies);

obsolete (see 60abd1e94168);

more robust after shutdown;

more sequential access to Session.manager.global_state: avoid minor divergence of tip version;

clarified share_common_data: after finished checkpoint, before next edits;

obsolete (see 030a6baa5cb2 and d14ddb1df52c);

support headless_load_limit for more scalable load process;

added dump_options: disabled by default;

tuned message;

clarified incremental loading: requirements based on maximal nodes;

tuned signature;

tuned;

tuned message;

more explicit type Load_State;

more operations -- incremental exploration of reachable nodes;

tuned messages (again) -- avoid confusion wrt. total remaining size;

added lemma

more Phabricator configuration;

A little more material from the Fourier AFP entry, and the correction of two very slow proof lines

boot with Phabricator PHP daemon;

clarified sshd setup: standard service on non-standard port 222, special "vcs" service on standard port 22;

disable lrzcloud1 -- superseded by lrzcloud2;

merged

replaced new type ('a,'b) tree by old type ('a*'b) tree.

more Phabricator configuration;

merged

merged

simplified proofs

some information about Phabricator server setup;

More type class generalisations. Note that linorder_antisym_conv1 and linorder_antisym_conv2 no longer exist.

merged

Enforced precodition "n <= length xs" to avoid relying on "hd []".

Generalisation of many theorems to a more abstract type class (suggested by Mr Anonymous)

tuned

added lemma

proper file name instead of font name (amending dc9a39c3f75d);

added function

merged

clarified data structures; eliminated presumably obsolete check of known_theories: should be unique by construction;

unused;

merged

Tidying and one more theorem

merged

explicit check of assumption prefix;

clarified signature;

clarified modules;

support soft types for 'have' etc., with careful export wrt. result text to avoid extra assumptions (details may differ due to polymorphism);

proper export of result_text for 'have';

support soft types for 'assume'; clarified "text": avoid polymorphism due to premature export;

more robust declaration of resulting statement text, instead of somewhat accidental (Variable.maybe_bind_term result_binds in generic_goal);

clarified modules;

clarified signature -- removed unused option (see acb0807ddb56);

one small last theorem

Four new results from Smooth_Manifolds/Analysis_More

A few more simple results

imported new material mostly due to Sébastien Gouëzel

A couple of new theorems, stolen from AFP entries

A few new theorems, tidying up and deletion of obsolete material

merged

more errors;

clarified inversion of file name to theory name, notably for Windows;

clarified import_name: observe directory notation more strictly;

tuned signature;

clarified signature -- removed pointless operations;

clarified signature -- removed unused content;

clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);

find theories via session directories only -- ignore known_theories;

tuned;

tuned message;

merged

tuned

A little-known material, and some tidying up

merged

tuned;

clarified theory status;

dump ZF in parallel to HOL Main;

tuned messages;

more ambitious options (again);

more ambitious options (again, after 93aa546ffbac);

tuned signature;

proper clean_theories wrt. dynamic dep_graph;

tuned signature;

potentially more robust: read under lock if not yet set;

tuned;

New theory Equivalence_Measurable_On_Borel, with the HOL Light notion of measurable_on and its equivalence to ours

session directories need to exist;

clarified signature: eliminated unused option;

merged

importation fix

merged

new material on Analysis, plus some rearrangements

eliminated pointless theory graph (reverting parts of a56eab490f4e): it caused problems with loaded vs. non-loaded node names, e.g. for theory Pure (see also 29bb1ebb188f);

discontinued obsolete "isabelle imports" and all_known data;

avoid duplicate directories wrt. synthetic session;

disallow accidental duplicates within the same session specification -- proper total match;

find theory files via session structure: much faster Prover IDE startup;

find theory node name via session directories;

disallow overlapping session directories;

tidied up some massive ugliness

clarified messages;

clarified syntax: 'directories' and 'theories' belong together;

more documentation;

check session directories;

declare session directories;

clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);

theory_name based on session_directories: no need for expensive all_known;

clarified session_directories: relative to session_path, with overlapping information;

clarified signature: retain global session information, unaffected by later restriction;

disable fragile options for now;

avoid overlapping session directories;

support for explicit session directories;

obsolete (see 94442fce40a5);

optional trace output;

prefer commands_accepted: fewer protocol messages;

prefer define_commands_bulk: fewer protocol messages;

clarified signature;

tuned signature -- prefer bulk messages;

tuned signature;

proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);

more robust;

unused;

proper finished_theory status for result;

more central checkpoint;

disable share_common_data for now (amending 0f8742b5a9e8) -- potentially more robust;

merged

load theories in stages, to reduce ML heap requirements;

more complete graph;

tuned messages;

tuned signature;

clarified signature;

tuned important special case;

tuned signature;

more dump_checkpoints;

clarified signature;

clarified state variable: avoid extra mutability via Promise;

Removal of the redundant ancestor Continuous_Extension

Half of Brouwer_Fixpoint split off to form a separate theory: Retracts.

Theory Derivative no longer depends on Path_Connected

more explicit type Dump.Session, with context information;

proper orientation;

clarified signature: prefer operations without position;

prefer Theory_Ordering theory names are unique (due to proper session context);

clarified signature: full dependency graph;

merged

more scalable isabelle dump (and derivatives): mark individual theories to share common data in ML;

tuned signature;

merged

simplified proofs

more rules for ordered real vector spaces

simplified setup

tuned proof

merged

enable share_common_data for "isabelle dump" and its derivatives (e.g. "isabelle mmt_import"): this has the potential to reduce ML heap size considerably, after initial command definitions;

support for share_common_data after define_command and before actual update: this affects string particles of command tokens;

more scalable -- less ML heap requirements;

tuned whitespace;

Integrate locale activation fallback diagnostics with 'trace_locales'.

entry point for analysis without integration theory

removed Brouwer_Fixpoint from imports of Derivative

removed unused lemma, generalized, reduced dependencies

fixed typo

moved lemmas; reduced dependencies of Lipschitz

explicit instance real::ordered_real_vector before subclass in ordered_euclidean_space

merged

moved lemmas