more standard method setup;

more precise declaration of goal_tfrees in forked proof state;

partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;

multiset operations are defined with lift_definitions; tuned proofs;

remove outdated comment

rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;

standardized ML aliases;

clarified proof_result: finish proof formally via head tr, not end_tr;

tuned;

more robust Future.fulfill wrt. duplicate assignment and interrupt;

tuned message;

always signal after cancel_group: passive tasks may have become active;

just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update; explicit terminate_execution; tuned source structure;

merged

moved lift_raw_const wrapper out of the Quotient-package into Nominal2

misc tuning and simplification;

static relevance of proof via syntax keywords;

tuned future priorities: print 0, goal ~1, execute ~2;

updated for Poly/ML SVN 1476;

some coverage of HOL/TPTP;

added graph-conversion utility for TPTP files

moved non-interpret-specific code to different module

disable parallel proofs (again) -- still suffering from instabilites wrt. interrupts;

tuned proofs;