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;