proper citation (amending d8205bb279a7);

proper citation (amending 98ba42f19995);

merged

prefer statically-typed close operation, avoid Java 11 warning: "Illegal reflective access by scala.reflect.package$ to method sun.net.httpserver.LeftOverInputStream.close()";

more robust hostname for Isabelle cronjobs: do not rely on target OS installation for resulting build_log database content;

more uniform wrt. File.find_files;

proper use of stat() vs. lstat() (for symlinks);

more uniform find_files, notably for symlinks;

is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;

clarified default (amending 72a9860f8602): avoid implicit change of File.find_files (it can have bad effects e.g. on "isabelle update_cartouches");

fixed import

extract example for ab_group_add_on_with

generalized local_typedef_ab_group_add

use locales in Group_On_With

more robust;

clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";

tuned;

more Haskell operations;

tuned signature;

clarified signature;

more Haskell operations; more accurate exports; tuned;

proper export;

tuned

merged

more [simp]

clarified display name;

added ML antiquotation @{master_dir};

tuned signature;

more formal references;

more Haskell antiquotations;

more Haskell operations;

support for user-defined Isabelle/Scala command-line tools; misc tuning and clarification;

replaced some ancient ASCII syntax

clarified status of legacy input abbreviations

clarified status of ancient ASCII syntax for big union and inter

NEWS;

isabelle update_cartouches -t;

update ROOT files as well: treated like .thy in Isabelle/jEdit;

clarified isabelle_fonts license, to be used when the component is updated next time;

tuned whitespace;

clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;

always insist in specified resolver/compiler version;

proper ML expressions, without trailing semicolons;

insist in specified resolver/compiler version;

simplified -- according to regular "ghci" script;

clarified ML positions (see also 1a52baa70aed);

more standard Resources.provide_parse_files: avoid duplicate markup reports;

more uniform (see 1722cc56d22e);

removed relics of ASCII syntax for indexed big operators

tuned;

obsolete;

clarified signature;

more uniform read_file_content for Isabelle/jEdit and Isabelle/VSCode: make_theory_content is required for semantic checking of user file-formats (e.g. bibtex);

more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;

merged

proper ghc_setup / ocaml_setup on target Isabelle distribution (amending 2a17c481d05e);

dedicated examples for sorting

more direct implementations of comparators

generic merge sort

merged

more Haskell operations;

tuned;

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;