introduced Simpdata structure

added Trueprop_conv

restructured some proofs

tuned keyword setup for SML code generator

moved order arities for fun and bool to Fun/Orderings

removed HOL structure

adjusted syntax for internal code generation

Added nominal_primrec command.

Adapted to new nominal_primrec command.

Added nominal_primrec.ML

Implemented new "nominal_primrec" command for defining functions on nominal datatypes.

Additional information about nominal datatypes (descriptor, recursion equations etc.) is now stored in theory.

converted legacy ML scripts;

Remove add_master_files which stripped paths for retracted files. Emacs PG already supports full paths here.

* Pure: syntax constant for foo (binder) is called foo_binder;

extend_trtab: allow identical trfuns to be overwritten;

tuned;

Binder: syntax const is determined by binder_name, not its syntax;

simplified consts: no auxiliary params, sane mixfix syntax; declarations: proper morphisms; added target_morphism/name;

abbrevs: no result; Element.map_ctxt_attrib;

added export_(standard_)morphism;

Element.map_ctxt_attrib;

abbrevs: no result; added target_morphism/name; simplified theory prefix (no option); proper morphing of abbrevs/notation;

added map_ctxt_attrib;

abbrevs: no result;

added morh_result, the_inductive, add_inductive_global; removed get_inductive; more careful treatment of result naming/morphing;

InductivePackage.add_inductive_global;

updated (binder) syntax/notation;

tuned morphisms;

added export_morphism; ProofContext.init;