isabelle-ml mode with separate token marker; clarified ML_Lex.gap_start: end-of-input counts as single newline;

partial scans via ML_Lex.tokenize_context; simplified ML_char: no gaps (hardly relevant in practice); tuned;

proper signature; removed dead code;

lexical syntax for SML (in Scala); tuned;

tuned;

removed dead code;

tuned signature (in accordance to ML version);

tuned proofs;

tuned signature -- separate Lexicon from Parsers (in accordance to ML version);

prefer latest ProofGeneral-4.2-1 by default;

updated thy_info.dependencies;

tuned message;

more integrity checks of theory names vs. full node names;

abstract type must be a type constructor; check it

generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated

better handling of recursion through functions

added examples/tests

tuned code to allow mutualized corecursion through different functions with the same target type

removed assumption in 'primrec_new' that a given constructor can only occur once

generate unique names

allow different functions to recurse on the same type, like in the old package

improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor

made N2M more robust w.r.t. identical nested types

register bnfs for (co)datatypes under their proper name (lost in af71b753c459)

updated keywords;

restored old 'remotify' logic -- too many bugs were introduced when refactoring the code

more (co)datatype docs

hide 'rel' name -- this one is waiting to be merged with 'list_all2'

updated docs to reflect the new 'free_constructors' syntax

more precise spec rules for selectors