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

tuned names

tuned

tuned

back to post-release mode;

Added tag Isabelle2019-RC2 for changeset 805250bb7363

fixed theory name

simplified types

clarified documentation;

more documentation;

merged

more NEWS;

tuned;

tuned;

proper formatting (amending 5076725247fa);

more on "Physical and logical files";

proper session chapter; cannot access session: refers to ROOT entry;

misc tuning;

more uniform scaling;

New version of tries

clarified InstallPath: relative to self-extracting exe; support for AutoInstall (option -ai);

prefer HTTPS;

eliminated old com.apple.eawt.FullScreenUtilities.setWindowCanFullScreen: appears to be unnecessary on newer versions of Mac OS X;

back to gz for linux (and macos) -- xz is too slow and cumbersome;