more system options as context-sensitive config options;

Thy_Output.modes as proper option;

some system options as context-sensitive config options;

system options as context-sensitive configuration options within the attribute name space;

tuned signature;

properly handle SPASS constructors w.r.t. partially applied functions

tuned signature -- depend on context by default;

reflexivity rules for the function type and equality

tuned comments

correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer

tuning

more work on SPASS datatypes

tuning -- renamed '_from_' to '_of_' in Sledgehammer

compile

don't recognize overloaded constants as constructors for the purpose of removing type arguments

tuning

reintroduced syntax for "nonexhaustive" datatypes

tuning

more work on SPASS datatypes

merged

setup for set membership as a predicate for code_pred

tuned

explicitly state equivalence relation for sim; tweak syntax of sem_equiv

merged

finally: acom with pointwise access and update of annotations

merged;

clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;

simplified ProofGeneral.preference operation -- no need for CRITICAL section for atomic access (and sequential execution of PG/TTY loop);

back to hidden welcome -- revert change 9ebf2da69b29, which appears to disturb startup protocol of PG 4.1;

more standard Isabelle/ML structures for global preferences; allow to add categories later on; allow to redefine preferences as usual for global tables, e.g. after reloading ML modules;

more basic print mode "ProofGeneral" (again);

uniform welcome -- actually visible on startup via Output.urgent_message; tuned;

more elementary ProofGeneral.thm_deps;

tuned;

moved files;

clarified default for Proofterm.proofs, according to etc/options and innermost setmp;

maintain ProofGeneral preferences within ProofGeneral module; initialize Isabelle/Pure preferences within normal user space (with antiquotations); tuned;

just one ProofGeneral module;

tuning

more work on SPASS datatypes

tuning

no need to reinvent the wheel ("fold_map")

more work on implementing datatype output for new SPASS

tuned code

compile

renamed Sledgehammer functions with 'for' in their names to 'of'

added datatype declaration syntax for next-gen SPASS

abstract equalities only in a correspondence relation in a transfer domain rule

superfluous transfer rule

stronger reflexivity prover

simplified modules and exceptions;

more elementary pgiptype;

prefer Markup.parse/print operations -- slight change of exception behaviour; removed obsolete PGIP material;

more uniform Markup.print_real;

removed dead code;

more uniform Markup.parse_real;

tuned signature;

more robust load_timings: ignore JVM errors such as java.lang.OutOfMemoryError;

tuned;

misc tuning and simplification;

more frugal line termination, to cope with huge log files (see also 016cb7d8f297);

more scalable File.write via separate chunks; tuned signature of File.write_xz: prefer defaults over overloading;

more scalable Library.separate -- NB: JVM has tiny fixed-size stack;

support for more informative crashes;

more antiquotations;

tuned messages;

more generous java resources via ISABELLE_BUILD_JAVA_OPTIONS;

generate valid direct Isar proof also if the facts are contradictory

tuned names

tuned names

removed obsolete PGIP material;

more direct output of remaining PGIP rudiments; tuned signature;

simplified preferences, removed obsolete operations;

tuned signature;

more direct output of remaining PGIP rudiments;

obsolete;

removed obsolete PGIP material;

recovered informative progress from 016cb7d8f297;

removed obsolete PGIP material;

clean startup of RAW session;

dummy PGIP id, which appears to be sufficient for PG/Emacs; removed obsolete init operations;

limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);

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]