tuned markup -- prefer user-perspective;

tuned specifications and proofs;

more precise type;

refined Markup_Tree implementation: stacked markup within each entry; tuned;

tuned signature; express select in terms of cumulate;

tuned signature;

merged

merged

abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite; add tests for abel_cancel simprocs

use simproc_setup for the remaining nat_numeral simprocs

use simproc_setup for more nat_numeral simprocs; add simproc tests

using more conventional names for monad plus operations

more tooltip content;

added markup_cumulate operator;

depth-first proof forking for improved locality (wrt. cancellation and overall memory usage);

tuned;

more abstract Markup_Tree;

prefer statically typed Text.Markup;

discontinued entity text color, notably historic red for classes; tuned entity names;

more scalable Proof_Context.prepare_sorts; reverted a97251eea458 -- uniform position constraints independently of accidental source positions (e.g. TTY vs. document);

increasing values_timeout to avoid failures of isatest with HOL-IMP

renaming example invocations: tester predicate_compile is renamed to smart_exhaustive

adding CPS compilation to predicate compiler; removing function_flattening reference; new testers smart_exhaustive and smart_slow_exhaustive; renaming PredicateCompFuns to Predicate_Comp_Funs;

adding option allow_function_inversion to quickcheck options

more efficient prepare_sorts -- bypass encoded positions;

suppress irrelevant positions;

more generous margin;

pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;

tuned signature;

discontinued unused Thm.compress (again);

renewed prolog-quickcheck

adding some test cases for preprocessing and narrowing

adding a minimalistic preprocessing rewriting common boolean operators; tuned

merged

merged

tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1

use simproc_setup for some nat_numeral simprocs; add simproc tests

add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type s not in this class); test simprocs using most general type classes instead of just int and rat.

simultaneous check; tight maxidx;

avoid separate typ_check phases, integrate into main term_check 0 instead (cf. its Syntax.check_typs in Type_Infer_Context.prepare);

clarified singleton_fixate: intersection with supersort is identity, only replace actual type inference parameters; tuned reject_other, after_infer_fixate;

misc tuning and simplification;

misc tuning;

tuned signature; tuned;

quickcheck invocations in mutabelle must not catch codegenerator errors internally

sort assignment before simultaneous term_check, not isolated parse_term; prefer Syntax.read_typ over Syntax.parse_typ, to include check phase for sort assignment; simplified Syntax_Phases.decode_sort/decode_typ; discontinued unused Proof_Context.check_tvar;

tuned;

avoid inconsistent sort constraints;

localized Record.decode_type: use standard Proof_Context.get_sort; clarified Record.varifyT: more convential use of maxidx + 1;

tuned signature -- emphasize internal role of these operations;

proper configuration option; tuned;

tuned layout;

more precise messages with the tester's name in quickcheck; tuned

quickcheck fails with code generator errors only if one tester is invoked

removing extra arguments

removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result

tuned

more fragments to export, removed the one from Com

updated functor Named_Thms; updated type attribute;

disabled Thm.compress (again) -- costs for building tables tend to be higher than potential benefit;