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;

simultaneous fact morphism;

added type_map;

added cterm_rule;

fake predeclaration of structure ProofContext;

added export_morphism;

ProofContext.init;

Comment: see RFC 2396 for relative URI syntax.

Send full paths in PGIP version of file loaded/retracted messages

Conversion of "equal" to "=" for TSTP format; big tidy-up

Lemma "fundef_default_value" uses predicate instead of set.

The function package declares the [code] attribute automatically again.

exported mk_base_funs for use by size-change tools