more direct Context.setmp_thread_data for one-way passing of context;

tuned;

tuned;

do not open ML structures;

prefer separate 'ML_command' for parallel evaluation;

simplified context and data management -- plain ctxt: Proof.context is default for most operations;

more conventional spelling and grammar;

minor tuning -- more linebreaks;

removed pointless comment -- NB: Isabelle output is message-oriented with implicit line-boundaries;

standardized aliases;

do not handle arbitrary exceptions;

added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;

merged

tuned signature;

tuned signature; tuned;

misc tuning;

prefer existing beta_eta_conversion;

more standard fold/fold_rev;

tuned import;

misc tuning;

prefer existing beta_eta_conversion;

more standard names;

simplified method setup;

tuned -- prefer terminology of tactic / goal state;

tuned;

misc tuning;

tuned;

tuned signature;