tuned color (cf. jEdit FUNCTION);

tuned;

more markup for inner syntax class/type names (notably for completion); explicit reports result without broadcast yet, which is important for brute-force disambiguation;

tuned proofs;

back to stable polyml-5.5.1, due to problems with Poly/ML SVN 1913 and HOL-Proofs (Fail "Insufficient memory");

more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;

unused;

special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;

more thorough (potentially duplicate) markup, e.g. relevant for embedded Args syntax within antiquotations;

suppress short abbreviations more uniformly, for outer and quasi-outer syntax; tuned signature;

clarified init_assignable: make double-sure that initial values are reset; more systematic reports for Args.syntax: indicate Args.$$$ quasi-keywords and suppress confusing completion of single symbols like ":", "|", "?";

proper UTF-8;

fix typo

remove simp rules made redundant by the replacement of neg_numeral with negated numerals

tuned proof

tuned proof script

no 'sorry' so that the schematic variable gets instantiated

removed junk

simplify sets in BNF composition

tuning

more caching in composition pipeline

register relator equations as spec rules only for datatypes -- for codatatypes they underspecify the function and are therefore dangerous (e.g. to Nitpick)

updated docs

renamed a pair of low-level theorems to have c/dtor in their names (like the others)

propagate the exception that is expected later on

N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;

merge

removed debugging leftover

minor doc fix

added contributor

simplified N2M code now that 'fold' is no longer used by the sugar layer + use right context in all 'force_typ' calls

fixed handling of 'case_prod' and other 'case' functions for interpreted types