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;

always preserve authentic consts -- removed Syntax.mixfix_const;

tuned;

removed outdated/redundant comments;

prefer 'definition' over low-level defs; tuned source/document;

tuned source/document;

hide const subst;