tuned layout;

tuned header;

updated version information;

removed outdated comment

adding examples for the potential counterexamples in the simple scheme

also potential counterexamples in the simple exhaustive testing in quickcheck

quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned

adding more verbose messages to exhaustive quickcheck

quickcheck narrowing also shows potential counterexamples

adding a exception-safe term reification step in quickcheck; adding examples

quickcheck returns counterexamples that are potentially spurious due to underspecified code equations and match exceptions

adding parsing of potential configuration to quickcheck command

adding quickcheck's potential configuration

more conventional file name;

merged

updated documentation for the quotient package

merged

alternative names of morphisms in the definition of a quotient type can be specified

adjusting antiquote_setup (cf. d83797ef0d2d)

clarified Time vs. Timing;

separate compilation of PIDE vs. Pure sources, which enables independent Scala library;

clarified modules;

tuned proofs;

rearranged files;

merged

use HOL_basic_ss instead of HOL_ss for internal simproc proofs (cf. b36eedcd1633)

explicit indication of modules for independent Scala library;

separate module for concrete Isabelle markup;

renamed Isabelle_Markup to Isabelle_Rendering to emphasize its meaning and make room for Pure Isabelle_Markup module;

tuned signature (according to ML version);

merged

Hide Product_Type.Times - too precious an identifier

more antiquotations;

tuned messages;

avoid stepping outside of context -- plain zero_var_indexes should be sufficient;

increasing timeout to avoid test failures

merged

merged

simplified Collecting1 and renamed: step -> step', step_cs -> step

more antiquotations;

tuned proof;

permissive update for improved "tool compliance"; tuned;

just one data slot per module; tuned;

tuned;

tuned;

more antiquotations;

misc tuning;

refined "literal" document style, with some correspondence to actual text source;

modernized section about congruence rules;

sharing of token source with span source;

memoing of forked proofs;

tuned;

removed obsolete argument (cf. 954e9d6782ea);

merged

removed obsolete uses of Local_Theory.restore -- package composition P1 #> P2 no longer requires them due to 57def0b39696: P2 finds the results of P1 in the auxiliary context

merged

tuned

increased stack limits (again, cf. d9cf3520083c and 77c3e74bd954);

explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;

tuned proofs;