tuned;

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;