removed Variable.monomorphic;

comments fixed, member function renamed

Change to algebra method.

Reimplemented algebra method; now controlled by attribute.

Strict dfs traversal of imported and registered identifiers.

added map_default, internal restructuring

export is_tid;

thm_of_proof: improved generation of variables;

Sign.infer_types: Name.context; FactIndex.add_local: simplified interface; Variable.constraints_of;

reorganize declarations (more efficient); renamed rename_wrt to variant_frees (avoid confusion with Term.rename_wrt_term, which reverses the result); tuned;

Name.context for used'';

added variant_frees; tuned;

tuned;

export make_context, is_declared;

prove: Variable.declare_internal (more efficient);

add_local: simplified interface, all frees are known'';

Sign.infer_types: Name.context;

renamed Variable.rename_wrt to Variable.variant_frees;

Fixed the bugs introduced by the last commit! Output is now *identical* to that produced by the old version, based on a-lists.

MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems

thm_of_proof: tuned Name operations;

print_statement: tuned Variable operations;

added newly_fixed, focus; removed monomorphic; tuned;

added declare_term_names; tuned;

fold_proof_terms: canonical arguments; removed obsolete add_prf_names, add_prf_tfree_names, add_prf_tvar_ixns;

Term.declare_term_names;

Started implementing uniqueness proof for recursion combinator (still unfinished).

typo (theorerms) fixed

typo (theorerms) fixed

AList.join now with 'DUP' exception

added Table.map_default

removed obsolete ML files;