renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")

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;

slightly faster default compilation of Isabelle/Scala;

more explicit last exec result;

dynamic propagation of node "updated" status, which is required to propagate edits and re-assigments and allow direct memo_result; discontinued odd "touched" field -- check given edits directly;

tuned;

simplified Future.cancel/cancel_group (again) -- running threads only; more robust update/cancel_execution: full join_tasks of group before exec state assignment; tuned signature;