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;

merged

back to gz for macos: more robust;

proper arguments for library build;

tuned;

clarified smlnj installations;

Added tag Isabelle2019-RC1 for changeset 9c60fcfdf495

updated to jdk-11.0.3+7;

update to lts-12.26 (stable branch);

more NEWS

merged

tweaked a definition

VSCode extension for official Isabelle release;

merged

clearout of some useless lemmas

merged

more bibtex fields;

clarified PIDE markup;

De-applying and combining lemmas to make structured proofs

clarified directory location;

more lemmas

more correct simulation of eigen context for generated Isar statements

more tidying and de-applying

merged

merged

huge de-apply effort

more uniform Isabelle splash screen -- avoid problems with jEdit splash and Java 11 on some Linux window managers;

yet more de-applying

more de-applying

more tidying up

A bit of de-applying

Algebraic closure: moving more theorems into their rightful places

moving around some material from Algebraic_Closure

merged

full proof of algebraic closure, by Paulo de Vilhena

merged

final tidying-up

further de-applying

removal of ASCII connectives; some de-applying

tuned -- according to main website;

more ambitious compression;

tuned signature;

completion for \<^const>, although it often requires an extra argument;

proper treatment of root as directory;

tiny bit of extra restructuring

some variable renaming

tweaks esp renaming Rep_preal

Massive restructuring; deleting unused theorems

merged

partial updating to eliminate ASCII style and some applys

Added embedding_map_into_euclideanreal; reduced dependence on Equivalence_Lebesgue_Henstock_Integration in Analysis theories by moving a few lemmas

sequential build_release: it uses some of the test machines for pre-built images;

getting rid of most apply steps

consolidated map2 clones

separate type class for bit comprehension

no need to maintain two separate type classes

clarified structure of theories

follow convention of bold local syntax

more use of existing locales

avoid separate type class for mere definitional extension

tuned name

clarified notation

added lemma

incorporated various material from the AFP into the distribution

backed out experimental b67bab2b132c, which slipped in accidentally

merged

added lemmas

moved subset_image_inj into Hilbert_Choice

Lindelöf spaces and supporting material

hierarchically inclusive named theorem collections

removed unused fact collections

eliminated type class

entry point for comprehensive word library

tuned theory names

integrated Bit_Comparison into Word corpus

tuned

prefer one theory for misc material

moved instance to appropriate place

tuned for release;

clarified goto_file (again): treat bad entry as plain file to open empty buffer instead of error (amending a8142ac5e4b6);

afford more examples;

obsolete -- this is quite fast;

Group theory developments towards proving algebraic closure (by de Vilhena and Baillon)

merged

markup fixes

merged

Towards a proof of algebraic closure (NB not finished)

tuned signature;

prefer ctyp operations;

meson: more cterm operations;

more ctyp operations;

tuned;

clarified: use existing Thm.dest_ctyp_fun (which is more strict);

prefer exception TYPE, e.g. when used within conversion;

tuned signature -- more ctyp operations;

clarified group of "main" library sessions;

tuned signature -- more ctyp operations;

merged

tuned signature: more operations;

backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is

tuned

more document structure

tuned

more abbrevs;

obsolete;

merged

updated documentation;

avoid Isabelle symbols in URL;

formal URLs;

tuned spacing;

modernized tags: default scope excludes proof;

report document tags as seen in the text (not the active tag of Thy_Output.present_thy);

support "tag" marker with scope;

tidying up messy proofs about group element order

merged

simpler and stronger proofs

tuned;

tuned;

merge plus tidied three proofs

merged

merged

type instantiations for poly_mapping as a real_normed_vector

visible hairline for cursor, even on OpenJDK 11 (amending 2fd73a1a0937);

tuned signature according to ML version;

strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");

added document antiquotation option "cartouche";

allow faster navigation of directory hierarchy (reverting 69465c3e3560);

more robust test: avoid spurious Interrupt (stack overflow?) due to List.fun_lub_parametric;

prefer local options;

tuned signature; tuned message;

clarified order;

merged

prod/sum fixes

Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context

tuned layout;

updated screenshots;

ignore odd warnings;

tuned whitespace;

merged;

updated for release;

merged

clarified build of standard heaps;

updated for release;

tuned message;

retain copy of required components;

option for build_sessions;

tuned;

support for platform-specific builds on remote server;

more robust: always (re)build platform application bundles;

The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale

merged

More homology material

common type class for distributive division

regenerated using isabelle regenerate_cooper

more explicit way to re-generate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML

some more explicit document structure

merged

new Homology target, depending on HOL-Algebra and HOL-Analysis

merged

NEWS on homology

First tranche of the Homology development: Simplices [dummy commit to run testboard again]

updated to bib2xhtml-20190409: current repository clone;

proper treatment of isabelle_fonts_hinted in etc/preferences (i.e. a change of the default option);

back to scala-2.12.7 (due to reports about problems with new Mac hardware / OS installations by Jasmin Blanchette and Dmitriy Traytel);

tuned -- prefer Isar command 'compile_generated_files';

back to more robust "standard" anti-aliasing (reverting f610115ca3d0): sub-pixel rendering can have odd color effects, even on high-end displays;

NEWS

merged

bundle for cardinal syntax

better accessibility of directory content by typing name prefix;

uniform JVM heap options for Isabelle/Scala tools and scalac (again);

proper etc/preferences;

notes about old Java 8 font rendering for low-quality displays;

obsolete -- was mostly about 'export_code';

support both hinted and unhinted fonts;

option to bypass ttfautohint for experimentation (it can have adverse effects);

clarified settings: allow for more Java versions;

proper default;

clarified;

auxiliary operation for common uses of 'compile_generated_files';

merged

Free_Abelian_Groups finally working; fixed some duplicates; cleaned up some proofs

merged

fixes for Free_Abelian_Groups

updated screenshot;

more NEWS;

tuned;

merged

tuned;

documentation for generated files;

tuned;

type Path.binding may be empty: check later via proper_binding; clarified 'export_prefix' default;

clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure; tuned concrete syntax;

proper .exe path for export;

updated to sqlite-jdbc-3.27.2.1;

added command 'compile_generated_files'; tuned signature;

tuned signature: more operations;

tuned signature;