merged

option "goals_limit", with more uniform description;

clarified message when subgoals have been stripped -- unconditional;

retain goal display options when printing error messages, to avoid breakdown for huge goals;

typo

better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal

try to detect assumptions of transfer rules that are in a shape of a transfer rule

publish a private function

tuned names

re-init ISABELLE_PROCESS_OPTIONS to allow nested ISABELLE_PROCESS invocations, e.g. HOL-Mutabelle-ex;

more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;

prefer standard Isabelle/ML operations;

some system options as context-sensitive config options;

load options for regular isabelle-process, not just for Isar loop (relevant for numerous low-level tools) -- NB: Isabelle_Process manages options via protocol message;

support for system options as context-sensitive config options;

tuned signature;

tuned comments;

support for options as preferences;

more operations in accordance to Scala version;

more systematic access to options default;

full default options for Isabelle_Process and Build;

decentralized historic settings;

removed obsolete test_markup; tuned;

Proof General interaction always uses Isar loop; pass Isabelle/Scala options to Proof General process as well;

proper context;

merged

more direct PGIP/Emacs processing and output;

more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;

removed redundant modules;

removed some obsolete PGIP/PGEclipse material;

never open structure Unsynchronized (cf. "implementation" manual);

prefer explicitly qualified exceptions, which is particular important for robust handlers;

avoid PolyML.makestring, even in dead code;

fixed bug introduced when reintroducing set constructor, and visible when applying <= to 2- or more-ary relations, e.g. "(R::'a=>'a=>bool) <= R"

don't apply an unnecessary morphism

tuned

relator coinduction for codatatypes

standard ivl notation [l,h]

merged

tuned

avoid polymorphic uncurried aliases with more arguments than there are arguments in the most general type of a HOL constant, to dodge issues at declaration time

proper unmangling -- the bug is visible when "uncurried_aliases" is enabled with Alt-Ergo or Poly. SPASS

use right default for "uncurried_aliases" with polymorphic SPASS

relator induction for datatypes

store proper theorems even for fixed points that have no passive live variables

stronger monotonicity property for relators

make tactic actually work for op = as relator

tuned

hide Fin on output

removed dead argument

more robust iterator construction (needed for mutualized FPs)

tuning

removed dead internal constants/theorems

removed tracing

export one more function

added field to record

tuning

removed dead code

move function to library

tuning