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;

tuned signature;

clarified signature: more explicit operations for corresponding Isar commands;

proper URL;

fixed markup in Poly_Mapping; Free_Abelian_Groups (but not yet imported by Algebra!)

More group theory. Sum and product indexed by the non-neutral part of a set

theory Poly_Mapping

new theory Library/Poly_Mapping, of almost-everywhere-zero functions

Material concerning exact sequences of groups

Products and sums of a family of groups

new group theory material, mostly ported from HOL Light

UHD is standard, HD non-standard;

updated for release;

merged

Added tag Isabelle2019-RC0 for changeset 6f2ab7f150f6

updated for release;

eliminated hard TABs;

updated for release;

tuned;

The order of a group now follows the HOL Light definition, which is more general

merged

merged

some new group theory results: integer group, trivial group, etc.

more convenient export;

misc tuning for release;

more material for release;

misc tuning for release;

'code_reflect' only supports new-style 'file_prefix'; avoid fragile file "$ISABELLE_TMP/rat.ML";

tuned signature -- more exports;

tuned signature;

A few results in Algebra, and bits for Analysis

experimental commands for proof sketching and exploration

irrelevant

more PIDE markup and hyperlinks;

clarified signature: more explicit type Path.binding; tuned;

more LaTeX symbols;

tuned signature -- more operations;

tuned signature;

clarified 'file_prefix';

clarified style: allow to search PDF for keywords containing "_";

"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports; "export_code ... file" is legacy, the empty name form has been discontinued; updated examples;

removed junk;

clarified diagrams;

clarified diagrams;

proper syntax diagrams; tuned whitespace;

tuned names;

tuned whitespace;

proper local_theory command;

more exports: avoid clones in AFP;

tuned;

export_code/check_code formally updates the theory -- this opens further possibilities concerning Generated_Files; tuned;

tuned whitespace;

merged

more informative Spec_Rules.Equational: support corecursion;

more operations;

more stuff from HOL Light: Euclidean spaces and n-spheres, Hausdorff spaces, etc.

merged

more informative Spec_Rules.Equational, notably primrec argument types;

clarified signature: avoid direct comparison on type rough_classification;

tuned proofs;

removed spurious debugging;

export propositional status of consts;

merged

generalised homotopic_with to topologies; homotopic_with_canon is the old version

follow up on Braun: get timing function right

Tweak Braun tree list_fast_rec recursion. A minor adjustment simplifies the termination argument slightly.