prefer typedef without extra definition and alternative name; tuned proofs;

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;