accumulate status as regular markup for command range; tuned signature;

corrected slip

tuned

restore convenient code_abbrev declarations (particulary important if List.set is not the formal constructor for sets)

moved lemmas about List.set and set operations to List theory

moved lemmas about List.set and set operations to List theory

incorporated various theorems from theory More_Set into corpus

consolidated various theorem names relating to Finite_Set.fold and List.fold combinators

merged

farewell to theory More_List

dropped unused nth_map

more explicit NEWS

refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x";

tuned;

improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup; tuned;

tuned -- more direct @{type_name set} (NB: binder_tr' retains the original non-syntax type for the bound/free variable);

recovered case syntax for of_int, also with source positions (appears to be unused nonetheless);

more careful treatment of outermost constraints, e.g. constructors without arguments (despite loss of positions for catch-all variables);

proper refs;

incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)

incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes

prefer listsum over foldl plus 0

prefer concat over foldl append []

tuned proofs

interaction of set operations for execution and membership predicate

cleanup of code declarations

discontinued Syntax.positions -- atomic parse trees are always annotated;

improved case syntax: more careful treatment of position constraints, which enables PIDE markup; tuned;

misc tuning;

prefer raw_message for protocol implementation;