explicit is better than implicit

localized interpretation of min/max-lattice

adapted to localized interpretation of min/max-lattice

SUBPROOF/Obtain.result: named params;

updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;

advanced retrofit, which allows new subgoals and variables; added FOCUS -- does not require closed proof;

Variable.focus: named parameters;

lambda/cabs/all: named variants;

Goal.finish: explicit context for printing;

fixed Method.Basic;

eliminated obsolete/obscure Seq.wrap, Position.setmp_thread_data_seq;

Method.Basic: no position;

basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context; Method.Basic: no position;

dequeue_towards: need to try imm_preds as well;

internal session timing;

enqueue: maintain transitive closure, which simplifies dequeue_towards;

ML_Context.the_generic_context;

eliminated redundant Library.multiply;

renamed structure Display_Goal to Goal_Display;

tuned tracing;

added Multithreading.real_time;

simplified/unified Multithreading.tracing_time; tuned;

get_name: cover only PThm, not PAxm;

eliminated OldGoals.read_term;

more antiquotations instead of adhoc ML stuff;

ML_Context.the_local_context;

eliminated the_context;

do not open OldGoals;

renamed functor SplitterFun to Splitter, require explicit theory;

renamed functor BlastFun to Blast, require explicit theory; eliminated src/FOL/blastdata.ML;

eliminated OldGoals.prove_goal;

explicit OldGoals;