more robust: check archive ident;

misc tuning and clarification;

tagged 8 theories for the Analysis manual.

merged

more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;

more portable tar_options;

check (non-)executable files -- and eliminate them manually from the repository)

eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting; eliminated "isabelle news"; roper title in NEWS.html; more robust build of documentation, using proper Other_Isabelle settings: avoid conflict with enclosing ISABELLE_OCAML / ISABELLE_GHC; misc tuning and clarification;

tuned signature;

tuned signature;

updated PLATFORMS;

uniform naming of strong congruence rules

added lemma

update MacOSX plugin for Java 11;

Jenkins: run ghc_setup

clarified errors;

more robust: explicit version;

more robust: avoid implicit setup (with default resolver);

more portable;

proper path;

tuned;

merged

avoid strict evaluation of "isabelle_stack path --programs";

enforce settings that are likely to be outdated, e.g. in $ISABELLE_HOME_USER/etc/settings;

support for GHC via command-line tools;

tuned;

tuned message;

auto update;

isabelle_stack as portable shell function;

tuned;

added Array files

new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml

more intuitive and simpler (but slower) proofs

more material on finite maps

back to jdk-8u181: avoid degraded font-rendering of jdk-11 on Linux;

added simp-lemma

allow to switch ISABELLE_OCAML_VERSION later on; simplified command-line: no user args;

merged

Jenkins: run ocaml_setup

added simp-lemma

support for OCaml via command-line tools;

isabelle_opam as portable shell function;

added Braun_Tree.thy

activate jdk-11

updated xstream.jar to 1.4.10 for Java 9/10/11 (see http://x-stream.github.io);

updated to jdk-11: jre is only a symlink to jdk;

support for jdk-11;

updated to jdk-11;

generalization due to Alexander Maletzky

discontinue java.ext.dirs for jdk-11 -- in contrast to 982f0bf34804 for jdk-8;

more [simp]

avoid TCP_NODELAY (in contrast to 18c621069bf8): might cause problems with some versions of Ubuntu 18.04;

merged

updates to Algebra from Baillon and de Vilhena

use correct hostname

Jenkins: detect machine; adjust job parameters accordingly

Jenkins: tuned profiles

merged

simplified proofs

Jenkins: delete obsolete profile

tuned

merged

unused -- avoid illegal access in Java 11;

misc tuning and modernization;

merged

merged

cosmetic change to mvt

shuffle -> shuffles

shuffle -> shuffles

updated windows_app to launch4j 3.12: "fully supports Java 9 and newer";

explicit group "no_doc" for unfinished documentation, allows to suppress everything uniformly: -X doc -X no_doc;

reduce tracing messages to make it work in PIDE session;

unbounded tracing for proper termination, e.g. relevant for theory Sequents.Hard_Quantifiers;

tuned output -- avoid bombing of Scala toplevel, e.g. for AFP deps;

more direct implementation of distinct_subgoals_tac -- potentially more efficient;

tuned;

HOL-SPARK .prv files are no longer written to the file-system;

updated to postgresql-42.2.5;

merged

fix (non-existent) document generation

updated to scala-2.12.7;

news

de-emphasize HOL-SPARK: somewhat outdated;

proper naming conventions for contexts;

permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;

tuned spelling;

tuned whitespace and sections;

tuned -- eliminated clone;

suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);

obsolete (see 6f8ae6ddc26b);

updated to new list_update precedence

avoid confusing precedences

more direct locale goal: avoid renaming of type_parameters;

adapted to Library/LaTeXsugar

const_typ also works for fixed variables - useful primarily for locales

tuned message according to ML version;

more liberal: detect free-form infixes as well, e.g. Orderings.ord_class.less_eq;

more accurate syntax: e.g. avoid brackets as prefix notation;

more approximative prefix syntax, including binder;

proper syntax for locale vs. class parameters;

simpler def

tuned signature;

tuned signature;

provide CakeML component

clarified get_infix: avoid old ASCII input syntax;

remove dubious import

export locale dependencies, with approx. morphism as type/term substitution;

tuned signature;

merged

NEWS

more conversion from ( * ) to (*)

Prefix form of infix with * on either side no longer needs special treatment because (* and *) are no longer comment brackets in terms.

expose locale_dependency information;

tuned signature;

tuned signature: more explicit types;

tuned;

tuned signature: prefer value-oriented pretty-printing;

tuned signature;

tuned signature: prefer value-oriented pretty-printing;

tuned (according to signature);