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;

replaced butlast by Library.split_last;

replaced butlast by Library.split_last; removed dead code;

butlast removed (use fst o split_last instead)

support for MiniSat proof traces added

support for MiniSat proof traces added

has_consts renamed to has_conn, now actually parses the first-order formula to avoid problems caused by connectives buried within descriptions and set comprehensions.

function butlast added

Replaced a-lists by tables to improve efficiency

Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.

Only include combinators if required by goals and user specified lemmas. Remove a clause if too general.

Term.term_lpo takes order on terms rather than strings as argument.

keep/transaction: unified execution model (with debugging etc.); tuned;

trivial whitespace changes

simp method: depth_limit;

"conjecture" must be lower case

tuned insert_list;

Name.context already declares empty names; tune ins_sorts -- sort assigments should never change later;

strip_abs_eta: proper use of Name.context;

do not export make_context; initial context: declare empty names; variants: no special treatment of empty names;

removed colon from sym category;

fix to refl_clause_aux: added occurs check

* Isar: ":" (colon) is no longer a symbolic identifier character;

removed duplicate of Tactic.make_elim_preserve;

removed obsolete adhoc_freeze_vars (may use Variable.import_terms instead);

exported make_elim_preserve;

prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars; tuned;

simplified prove_conv;

removed ':' from category of symbolic identifier chars;

query/bang_colon: separate tokens;

purged website sources

added strip_abs_eta