caret_range based on BreakIterator, which handles combined unicode characters as well;

misc tuning;

some localization;

eliminated some legacy operations;

more antiquotations;

tuned whitespace;

eliminated some legacy operations;

removed dead code, which has never been active in recorded history;

do not open ML structures;

tuned signature;

hide quickcheck constants Abs_cfun and Rep_cfun, to avoid clash with HOLCF

hiding internal constants and facts more properly

removing catch_match' now that catch_match is polymorphic

adapting exhaustive generators in record package

outputing if counterexample is potentially spurious or not

making catch_match polymorphic

compilations return genuine flag to quickcheck framework

extending quickcheck's result by the genuine flag

reporting random compilation also catches match exceptions internally

the narrowing also indicates if counterexample is potentially spurious

the simple exhaustive compilation also indicates if counterexample is potentially spurious;

quickcheck-random compilation also indicates if the counterexample is potentially spurious or not

changing the exhaustive generator signatures; replacing the hard-wired result type by its own identifier

quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception

adding examples for quickcheck-random

removing exception handling now that is caught at some other point; tuned message

quickcheck random can also find potential counterexamples; moved catch_match definition; split quickcheck setup;

merged

merged IMP/Util into IMP/Vars

use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure

cardinality of sets of lists

do not import examples Probability theory

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;

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;

retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;

prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import; prefer non-strict lazy over strict future;

recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;

proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);

improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory

in a local context, also the free variable case needs to be analysed default tip

speed-up proof;

more abstract datatype stamp, which avoids pointless allocation of mutable cells;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;