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

moved basic theorem

proper positions for 'termination' command (see also 5549e686d6ac);

tuned names -- proper scopes;

added system option "execution_eager": potentially reduce resource requires for "isabelle mmt_import" (smaller subgraphs are finished and disposed earlier);

proper positions for 'termination' command instead of original 'function' command, e.g. relevant for isabelle mmt_import;

Tracing of locale activation.

tuned

always export Pure proofs;

clarified 'thm_deps' command;

more compact: avoid pointless PThm rudiments;

clarified signature: prefer total operations;

proper graph traversal: avoid multiple visit of unnamed nodes;

more scalable: avoid huge intermediate XML elems;

more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;

NEWS;

merged

export thm_deps;

proper theory context;

clarified thm_id vs. thm_node/thm: retain theory_name; support for thm_deps: expand unnamed nodes;

clarified signature;

tuned;

unused (see 095dadc62bb5);

tuned;

tuned signature;

clarified modules;

clarified modules;

tuned;

clarified signature;

tuned

tuned

merged

tuned

merged

clarified signature;

clarified export of axioms and theorems (identified derivations instead of projected facts);

tuned signature;

back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;

module Thm_Name for Isabelle/Scala;

tuned;

clarified modules;

tuned;

tuned

tuned names

clarified signature;

discontinued peek_status: unused and not clearly defined;

more documentation on oracles;

proper theory context for global props;

more thorough check, using full dependency graph of finished proofs;

added ML antiquotation @{oracle_name};

more robust, notably for open_proof of unnamed derivation;

tuned comments;

NEWS;

more accurate proposition for cheat_tac (command 'sorry');

added command 'thm_oracles';

clarified type for recorded oracles;

unused;

clarified signature;

clarified modules;

clarified lookup operations: more scalable for multiple retrieval;

clarified signature;

merged

maintain thm_name vs. derivation_id for global facts;

clarified identity of PThm nodes: do not reuse old id after renaming -- enforce uniqueness of substructures;

clarified signature;

Fixed brace matching (plus some whitespace cleanup)

merged

new material on eqiintegrable functions, etc.

clarified treatment of individual theorems; tuned messages;

tuned signature;

clarified signature;

clarified derivation_name vs. raw_derivation_name;

merged

more careful treatment of hidden type variable names: smash before zero_var_indexes to get standard enumeration;

more careful treatment of standard_vars: rename apart from existing frees and avoid approximative Name.declared, proper application of unvarifyT within terms of proof;

support Export_Theory.read_proof, based on theory_name and serial;

clarified PThm: theory_name simplifies retrieval from exports;

Indexname.toString according to string_of_vname' in ML;

clarified type Indexname, with plain value Int; eliminated pointless cache_int;

more complete pattern match;

export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;

support for (fully reconstructed) proof terms in Scala; proper cache_typs;

new material; rotated premises of Lim_transform_eventually

clarified name context for abstractions -- in contrast to 367e60d9aa1b and Term.variant_frees (*as they are printed :-*);

tuned;

uniform standard_vars for terms and proof terms;

treat simproc results as atomic -- more compact proof terms;

tuned;

minor performance tuning;

NEWS and example for Theory.join_theory;

tuned whitespace;

more compact proof terms;

more documentation;

added SUBPROOFS / "subproofs" method combinator, for more compact proofterms;

clarified modules;

merged

more compact proof terms;

more robust -- notably for metis, which tends to accumulate tpairs;

tuned -- avoid shadowing of ML names;

tuned;

more compact proof terms;

tuned;

tuned;

tuned -- eliminated unused parameters;

more direct/compact export of proof terms;

output physical_stderr, e.g. for low-level debugging;

tuned;

do not open ML structures;

tuned;

misc tuning -- slightly more readable;

simplified defs (thanks to Mohammad)

record sort constraints unconditionally: minimal performance implications;

more careful export of unnamed proof boxes: avoid duplicates via memoing;

tuned signature;

export each PThm node separately: slightly more scalable;

allow duplicate exports via strict = false;

tuned message;

more positions;

more positions;

tuned;

formal position for PThm nodes;

clarified ML types;

proper treatment of body oracles, outside of recursion into thms graph;

prefer named lemmas -- more compact proofterms;

prefer named lemmas -- more compact proofterms;

tuned whitespace -- slightly more readable;

clarified signature: fewer warnings in ML IDE;

tuned;

prefer named lemmas -- more compact proofterms;

more compact proofterms;

eliminated pointless comments;

clarified proofterms;

more robust and convenient treatment of implicit context;

removed junk (cf. fa933b98d64d);

explicit check of left-over constraints from different theory, e.g. due to lack of Thm.trim_context;

more careful treatment of implicit context;

more careful treatment of implicit context;

proper build options;

merged

backed out changeset 1b8858f4c393: odd problems e.g. in CAVA_LTL_Modelchecker;

more careful treatment of implicit context;

clarified signature; more careful treatment of implicit context;

more robust and convenient treatment of implicit context;

clarified context: proper transfer;

tuned;

clarified modules: more direct data implementation;

Added Takeuchi function to HOL-ex

full AFP test on lrzcloud2;

obsolete;

more efficient data structure;

clarified signature;

guard constraints by record_proofs=1, until performance implications have become more clear;

more complete completions according to Sorts.insert_complete_ars (cf. 13199740ced6), e.g. relevant for theories HOL-ex.Word_Type, HOL-Matrix_LP.SparseMatrix;

tuned;

tuned;

maintain sort constraints from type instantiations, with pro-forma derivation to collect oracles/thms; tuned;

more direct proofs for type classes; misc tuning and cleanup;

tuned;

clarified modules: inference kernel maintains sort algebra within the logic;

more elementary treatment of standard_vars (unconstrainT is already standard);

clarified module structure;

simplified module structure: back to plain datatype (see 95f4f08f950f and 70019ab5e57f);

abstract type theory_id -- ensure non-equality type independently of implementation;

clarified export: retain proof boxes as local definitions -- more scalable;

reduced dependencies

clarified global theory context;

more robust export, based on reconstruct_proof / expand_proof;

clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;

tuned -- fewer warnings;

discontinued pointless messages;

clarified context;

clarified modules;

discontinue clean_proof: without type args its PThm nodes are not expanded, but with type args it is too unstable;

merged

more diagnostic operations;

tuned -- non-strict args;

proper constrains_map -- for shyps that are covered by present variables (amending 251f1fb44ccd);

tuned signature;

clarified signature; tuned;

tuned signature;

News for bind infixl

Monadic bind is now infixl as is the norm

purge remains from test (cf. 5a53724fe247);

tuned;

clarified signature;

removed obsolete RC tags;

tuned;

clarified signature;

tuned;

tuned;

clarified signature;

tuned;

tuned;

tuned;

tuned -- reorder sections;

tuned;

proper argument type (amending 42fbb6abed5a);

tuned signature;

tuned;

finalize proofs earlier to reduce memory requirement;

proper proof_serial;

more explicit type proof_serial;

defer rew_proof on unnamed PThm node as open_proof operation: significant performance improvement; misc tuning and clarification;

more accurate proof definitions (PThm nodes);

avoid duplicate Thm.name_derivation on unnamed PThm nodes ("simps" vs. "case_eqns" and "recursor_eqns");

prefer local counter;

more accurate proof export;

clarified syntax;

tuned;

more thorough clean_proof;

clarified modules;

avoid global syntax for MinProof (amending e31271559de8);

treat MinProof like Promise before 725438ceae7c, e.g. relevant for performance of session Corec (due to Thm.derivation_closed/close_derivation);

discontinued Proofterm.Promise (cf. 725438ceae7c);

clarified treatment of unnamed PThm nodes (from close_derivation): retain full proof, publish when named; added Proofterm.clean_proof as simplified version of Reconstruct.expand_proof;

tuned comments;

proof terms are always constructed sequentially; discontinued unused Proofterm.Promise -- too complex;

tuned comments -- proper sections;

support export_proofs, prune_proofs; tuned comments;

clarified postproc: apply shrink_proof last, e.g. relevant for export of full proof term;

tuned;

clarified exception;

tuned;

more accurate type information;

unused (see also 42fbb6abed5a);

discontinued ASCII syntax;

global declaration of abstract syntax for proof terms, with qualified names; clarified modules;

tuned;

tuned;

more operations: support type classes within the logic;

clarified export of sort algebra: avoid logical operations in Isabelle/Scala;

more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);

more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;

More results about measure and integration theory

More analysis / measure theory material

merged

more new material about analysis

added forgotten declaration provided by Florian Haftmann

merged;

updated to jedit_build-20190717: support more brackets;

updated to isabelle_fonts-20190717;

redundant;

tuned;

added \<llangle>, \<rrangle>; discontinued special rendering for old {* *};

tuned doc isar-ref;

added \<bbar>;

added \<sqdot>;

fixed renaming issues

merged

a few new lemmas and a bit of tidying

support for a soft-type system within the Isabelle logical framework;

tuned

proper theory naming after join (reset due to merge_data);

support join of anonymous theory nodes, e.g. relevant for parallel theory construction;

clarified history stage: allow independent updates that are merged later;

support abstract syntax for proof terms (see src/Pure/Proofs/proof_syntax.ML);

proper quasi-total merge

made LaTeX happy

streamlined setup for linear algebra, particularly removed redundant rule declarations

tuned

tuned

even more appropriate fact name

more correct indicator

make latex happy

moved some theorems into HOL main corpus

misc tuning and modernization

more theorems for proof of concept for word type

official fact collection sign_simps

tuned proofs

avoid pseudo-collection to be used in generated proofs

moved comment to approproiate place

removed outcommented example which seems not to work as advertized

clear separation of types for bits (False / True) and Z2 (0 / 1)

generalized type classes for parity to cover word types also, which contain zero divisors

slightly more specialized name for type class

dropped weaker legacy alias

slightly more stringent ordering of theorems

removed relics of ASCII syntax for indexed big operators

dropped former legacy input abbreviations

using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax

prefer fixed simpset for proof procedure

tuned file system structure

avoid spammed sledgehammer proofs

added lemmas

proper URL;

merged;

Added tag Isabelle2019 for changeset 83774d669b51

handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)

tuned;

tuned;

backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;

unused;

tuned messages;

proper context;

misc tuning and clarification, notably wrt. flow of context;

proper context;

proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);

unused;

misc tuning and clarification, notably wrt. flow of context;

proper context;

proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);

more structural integrity;

tuned;

more structural integrity;

clarified transfer_morphism: implicit join_certificate, e.g. relevant for complex cascades of morphisms such as class locale interpretation;

tuned;

clarified signature;

tuned whitespace;

clarified context: prefer abstract Variable.auto_fixes;

tuned;

tuned signature;

redundant: default is false;

tuned imports -- accommodate scala-2.13.0-RC3;

tuned -- accommodate scala-2.13.0-RC3;

merged

Added tag Isabelle2019-RC4 for changeset ad2d84c42380

hint on printing via Web browser;

tuned;

tuned proof

tuned

merged

more direct invocation of Windows exe: avoid extra bash, cygpath, exec;

tuned whitespace;

updated to bash_process-1.2.3: rebuild on current reference PLATFORMS;

Added tag Isabelle2019-RC3 for changeset 85de4fdec61b

more robust InstallPath (amending 4ce07be8ba17): self-directory may be odd temp dir produced by browser "Run" operation;

avoid extra subprocess -- potentially more robust on Cygwin;

updated to cygwin-20190524;

proper version;

tuned spelling;

more thorough assignment, e.g. when "purge" removes commands that were not assigned;

tuned whitespace;

tuned signature (following Scala version);

tuned;

obsolete (incompatible with Isabelle2019);

amended to unoverload actually all parameters of a type variable

proper message;

Finite_Map: move lemmas from LambdaAuth AFP entry credits: Matthias Brun, Dmitriy Traytel

documentation for termination_simp attribute

strengthened lemma

tuned names

tuned name

tuned

a few general lemmas

Generalisations involving numerals; comparisons should now work for ennreal

tuned