Now the setup for cancel_numerals accepts mixed Sucs/+ where the Sucs no longer need to be outermost.

Tuned signature of Locale.add_locale(_i).

simplified mg_domain (use Sign.classes/arities_of); removed unused lift_local_theory_yield;

made $$ and "this" monomorphic (string);

tuned;

export arities_of instead of classes_arities_of;

updated;

renamed const less to lt;

renamed constant less in lattice

fixed problem with proof reconstruction by adding add_Suc to arith-simpset.

added parser locale_expr_unless

fixed clsvar bug

add_locale(_i) returns internal locale name.

added example for operational classes and code generator

slight improvement in serializer, stub for code generator theorems added

Renamed setsum_mult to setsum_right_distrib.

Internal restructuring: local parameters.

renamed op < <= to Orderings.less(_eq)

New interface function parameters_of_expr.

add_inst_arity_i renamed to prove_arity.

rename_frees: treat trivial names; monomorphic: tuned invented names;

added singleton;

updated;

turned string_of_mixfix into pretty_mixfix;

added monomorphic; export hidden_polymorphism;

added 'print_statement' command;

added print_stmts;

added pretty_statement;

added command, keyword; added chunks2;

Output.add_mode: keyword component;