tuned;

tuned;

made smlnj happy;

wellformed: be less ambitious about structural containment; tuned;

Pure: update on overloaded defs;

Extended strong induction rule with additional freshness constraints.

add theorem cfcomp_strict

added add_deps, which actually records dependencies of consts (unlike add_finals); tuned;

tuned;

axiomatize class: Theory.add_deps;

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;