concrecte sorting algorithms beyond insertion sort

proper self_update for isolated host;

renovated macOS tests;

support remote_build_history with optional ghc_setup / ocaml_setup;

more robust: avoid isabelle_stack invocation in settings script (potentially slow or failing);

clarified names;

more Haskell operations; tuned;

support sub-directories, i.e. structure module names;

prefer symbolic path: it is potentially persisted;

tuned (see map_index);

tuned;

simplified proof, moved lemma, added lemma

more Haskell operations;

ported from src/Pure/General/value.ML;

Faster Braun tree functions

more lemmas

NEWS;

merged

tuned whitespace;

tuned message (e.g. see Options.save_prefs);

tuned whitespace;

support for Isabelle tools in Haskell;

tuned comments;

more operations;

support for Isabelle tool development in Haskell;

tagged a theory for the Analysis manual

more

too many clashes with "root" on reals

added and renamed functions

added an example

clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);

tuned;

tuned;

merged

tuned example;

added GHC.read_source: read Haskell source text with antiquotations; added "cartouche" antiquotation for ML string expressions as Haskell string literals;

tuned -- prefer GHC.print_codepoint;

support for GHC: string literals;

some support for UTF-8 (similar to Isabelle/Scala version);

clarified signature;

tuned name

add reconstruction by veriT in method smt

split SMT reconstruction into library

added lemmas

suppress "FreeMarker Template Language" file extension for the sake of SAD3/ForTheL;

merged

tuned names

more robust: allow log to be a symlink;

moved lemmas

tuned

tuned and added lemmas

avoid abbreviation that is used only locally

dedicated theory for sorting algorithms

merged

more combinatorics lemmas

proper environment for variable folding;

merged

NEWS;

updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv; proper update of jEdit environment -- avoid warnings in Java 11; activate jdk-11+28;

clarified ML position: proper markup for def/ref scopes (see also 162a4c2e97bc);

updated to jdk-11+28 from https://adoptopenjdk.net -- with proper font rendering on Linux;

proper completion for @{named_theorems};

executable comparators apt for sorting

tuned grammar

more and generalized lemmas

Jenkins: delete obsolete profile

Tagged some theories in HOL-Analysis

proper chapter;

tuned messages;

tuned signature;

tuned messages;

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