moved theorems about distribution to the definition; removed oopsed-lemma

rename finite_prob_space.setsum_distribution, it collides with prob_space.setsum_distribution

remove duplicate theorem setsum_real_distribution

clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;

updated Sledgehammer docs with new/renamed options

added "minimize" option for more control over automatic minimization

renamed "slicing" to "slice"

tuning

minor example tweak

renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";

updated markup conforming to ML side;

discontinued obsolete datatype "alt_names";

misc tuning;

merged

removed outdated comment moved back and updated (at the direct request of Christian Urban)

more stable introduction of the internally used unknown term

prefer typedef without alternative name;

prefer cpodef without extra definition;

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;

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;