simplified info/get_info; Rep/Abs: Theory.add_deps; tuned;

simplified TypedefPackage.get_info;

made smlnj happy;

pretty_full_theory: tuned output of definitions;

export plain_args; tuned wellformed, normalize;

Defs.specifications_of: lhs/rhs now use typargs;

removed unchecked'';

pretty_full_theory: defs;

specifications_of: lhs/rhs represented as typargs; export pretty_const; export dest; more precise checking of lhs patterns; more precise normalization; misc cleanup;

export raw_unifys, could_unifys;

made smlnj happy;

export raw_matches;

tuned Defs interfaces;

yet another re-implementation: . maintain explicit mapping from unspecified to specified consts (no dependency graph, no termination check, but direct reduction of specifications); . more precise checking of LHS patterns -- specialized patterns (e.g. 'a => 'a instead of general 'a => 'b) impose global restrictions;

removed obsolete partition (cf. List.partition); tuned;

class axiomatization: finals;

abs: precise typing;

added syntax for 'unchecked';

primrec (unchecked);

List.partition;

ax_derivs: precise typing;

pow: unchecked;

removed obsolete 'finalconsts';

* Pure: syntax 'CONST name' produces a fully internalized constant; tuned;

added CONST syntax; tuned interfaces;

export generic term_syntax;

consts: replaced early'' flag by inverted authentic''; tuned interfaces;

added mapping;

replaced early'' flag by inverted authentic'';

renamed CONST to CONSTANT;

removing the string array from the result of get_clasimp_atp_lemmas

const_syntax;