renamed expand_*_eq in HOLCF as well

expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets

merged

lower expectation in Reg exp example

renewing specification in example file; adding invocation in example file

handling collection of simprules as sets rather than as lists

stating errors in error messages more verbose in predicate compiler

raising an exception instead of guessing some reasonable behaviour for this function

using linear find_least instead of sorting in the mode analysis of the predicate compiler

adding code attribute to definition of equality of finite sets for executability of equality of finite sets

adapting example files

adding the Reg_Exp example

towards time limiting the prolog execution

adding IMP quickcheck examples

adding the CFG example to the build process

adding a List example (challenge from Tobias) for counterexample search

adding dependencies to IsaMakefile; increasing negative search limit for predicate_compile_quickcheck; adding tracing of introduction rules in code_prolog

disposed some old TODO/FIXME;

Document_View: select gutter message icons from markup over line range, not full range results; tuned;

tuned properties;

moved token markup tables to isabelle_markup.scala;

concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;

simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default; tuned Snapshot.convert/revert;

Document_View: more precise painting of gutter icons, only if line selection area is sufficiently large;

basic support for warning/error gutter icons;

Document_View: some markup for main inner syntax categories;

Command.State.accumulate: check actual source range;

Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;

highlight bad range of nested error (here from inner parsing);

Isar_Document.reported_positions: exclude proof state output;