2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-19 wenzelm 2009-11-19 future_result: purge flexflex pairs, which should normally be trivial anyway -- prevent Thm.future_result from complaining about tpairs;
2009-09-30 wenzelm 2009-09-30 PARALLEL_GOALS: proper scope for exception FAILED, with dummy argument to prevent its interpretation as variable;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-08-12 wenzelm 2009-08-12 added PARALLEL_CHOICE, PARALLEL_GOALS;
2009-07-28 wenzelm 2009-07-28 eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;
2009-07-26 wenzelm 2009-07-26 Goal.finish: explicit context for printing;
2009-07-25 wenzelm 2009-07-25 renamed structure Display_Goal to Goal_Display;
2009-07-23 wenzelm 2009-07-23 clarified pretty_goals, pretty_thm_aux: plain context; explicit pretty_goals_without_context, print_goals_without_context; tuned;
2009-07-20 wenzelm 2009-07-20 moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display;
2009-07-20 wenzelm 2009-07-20 Proof.future_proof: declare all assumptions as well; Proof.future_proof: removed spurious exception_trace (which might cause crash-by-interrupt); replaced Future.fork_local by Future.fork_pri (again, until group exceptions are propagated properly);
2009-07-19 wenzelm 2009-07-19 parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
2009-07-19 wenzelm 2009-07-19 more abstract Future.is_worker; Future.fork_local: inherit from worker (if available);
2009-07-19 wenzelm 2009-07-19 future_result: explicitly impose Variable.sorts_of again;
2009-03-12 wenzelm 2009-03-12 Assumption.all_prems_of, Assumption.all_assms_of;
2009-01-11 wenzelm 2009-01-11 added Goal.future_enabled abstraction -- now also checks that this is already a future task, which excludes interactive commands of the old toplevel;
2009-01-10 wenzelm 2009-01-10 added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
2009-01-04 wenzelm 2009-01-04 tuned protect, conclude: Drule.comp_no_flatten;
2009-01-04 wenzelm 2009-01-04 future proofs: back to Future.fork_pri ~1 for improved parallelism;
2008-12-16 wenzelm 2008-12-16 future proofs: Future.fork_pri 1 minimizes queue length and pending promises -- slight improvement of throughput, at the cost of a bit of parallelism;
2008-12-16 wenzelm 2008-12-16 Future.fork_pri;
2008-12-12 wenzelm 2008-12-12 future proofs: more robust check via Future.enabled;
2008-12-04 wenzelm 2008-12-04 future proofs: pass actual futures to facilitate composite computations;
2008-10-16 wenzelm 2008-10-16 prove_common: include all sorts from context into statement, check shyps of result; Drule.norm_hhf_eqs;
2008-10-01 wenzelm 2008-10-01 renamed promise to future, tuned related interfaces;
2008-09-25 wenzelm 2008-09-25 simplified Thm.promise; prove_common: proper context for promise_result;
2008-09-25 wenzelm 2008-09-25 prove: error with original thread position;
2008-09-23 wenzelm 2008-09-23 prove_multi: immediate;
2008-09-23 wenzelm 2008-09-23 added promise_result, prove_promise;
2008-06-14 wenzelm 2008-06-14 prove: full Variable.declare_term, including constraints;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-04-17 wenzelm 2008-04-17 prove_global: Variable.set_body true, pass context;
2008-04-12 wenzelm 2008-04-12 replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2007-11-05 wenzelm 2007-11-05 removed unused compose_hhf, comp_hhf;
2007-07-03 wenzelm 2007-07-03 moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
2007-06-19 wenzelm 2007-06-19 balanced conjunctions;
2007-06-18 wenzelm 2007-06-18 tuned conjunction tactics: slightly smaller proof terms;
2007-06-13 wenzelm 2007-06-13 renamed prove_raw to prove_internal; tuned;
2007-06-04 wenzelm 2007-06-04 added assume_rule_tac;
2007-05-10 wenzelm 2007-05-10 moved some Drule operations to Thm (see more_thm.ML);
2006-12-07 wenzelm 2006-12-07 reorganized structure Goal vs. Tactic;
2006-11-30 wenzelm 2006-11-30 added norm/close_result (supercede local_standard etc.);
2006-11-29 wenzelm 2006-11-29 COMP_INCR;
2006-11-24 wenzelm 2006-11-24 ProofContext.init;
2006-08-02 wenzelm 2006-08-02 normalized Proof.context/method type aliases; simplified Assumption/ProofContext.export; tuned;
2006-07-30 wenzelm 2006-07-30 Thm.adjust_maxidx;
2006-07-29 wenzelm 2006-07-29 prove: proper assumption context, more tactic arguments; tuned;
2006-07-27 wenzelm 2006-07-27 moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
2006-07-19 wenzelm 2006-07-19 prove: Variable.declare_internal (more efficient);
2006-07-08 wenzelm 2006-07-08 prove/prove_multi: context; prove_global: theory + standard; tuned;
2006-06-12 wenzelm 2006-06-12 Unify.matches_list;
2006-06-05 wenzelm 2006-06-05 allow non-trivial schematic goals (via embedded term vars);
2006-05-11 wenzelm 2006-05-11 check result against certified prop, i.e. admit non-normal statements;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-13 wenzelm 2006-04-13 use conjunction stuff from conjunction.ML;
2006-03-08 wenzelm 2006-03-08 tuned;
2006-03-05 wenzelm 2006-03-05 SELECT_GOAL: fixed trivial case;
2006-03-04 wenzelm 2006-03-04 added extract, retrofit;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;