src/Pure/goal.ML
Sat, 20 Mar 2010 17:33:11 +0100 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Thu, 19 Nov 2009 17:29:39 +0100 wenzelm future_result: purge flexflex pairs, which should normally be trivial anyway -- prevent Thm.future_result from complaining about tpairs;
Wed, 30 Sep 2009 22:26:47 +0200 wenzelm PARALLEL_GOALS: proper scope for exception FAILED, with dummy argument to prevent its interpretation as variable;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Wed, 12 Aug 2009 00:26:01 +0200 wenzelm added PARALLEL_CHOICE, PARALLEL_GOALS;
Tue, 28 Jul 2009 16:30:23 +0200 wenzelm eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;
Sun, 26 Jul 2009 13:12:52 +0200 wenzelm Goal.finish: explicit context for printing;
Sat, 25 Jul 2009 10:31:27 +0200 wenzelm renamed structure Display_Goal to Goal_Display;
Thu, 23 Jul 2009 16:52:16 +0200 wenzelm clarified pretty_goals, pretty_thm_aux: plain context;
Mon, 20 Jul 2009 21:20:09 +0200 wenzelm moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
Mon, 20 Jul 2009 00:37:39 +0200 wenzelm Proof.future_proof: declare all assumptions as well;
Sun, 19 Jul 2009 19:24:04 +0200 wenzelm parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
Sun, 19 Jul 2009 18:02:40 +0200 wenzelm more abstract Future.is_worker;
Sun, 19 Jul 2009 14:15:47 +0200 wenzelm future_result: explicitly impose Variable.sorts_of again;
Thu, 12 Mar 2009 15:54:58 +0100 wenzelm Assumption.all_prems_of, Assumption.all_assms_of;
Sun, 11 Jan 2009 18:18:35 +0100 wenzelm added Goal.future_enabled abstraction -- now also checks that this is already
Sat, 10 Jan 2009 21:32:30 +0100 wenzelm added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
Sun, 04 Jan 2009 15:28:40 +0100 wenzelm tuned protect, conclude: Drule.comp_no_flatten;
Sun, 04 Jan 2009 00:01:16 +0100 wenzelm future proofs: back to Future.fork_pri ~1 for improved parallelism;
Tue, 16 Dec 2008 18:04:16 +0100 wenzelm future proofs: Future.fork_pri 1 minimizes queue length and pending promises
Tue, 16 Dec 2008 16:25:19 +0100 wenzelm Future.fork_pri;
Fri, 12 Dec 2008 12:14:02 +0100 wenzelm future proofs: more robust check via Future.enabled;
Thu, 04 Dec 2008 23:00:58 +0100 wenzelm future proofs: pass actual futures to facilitate composite computations;
Thu, 16 Oct 2008 22:44:28 +0200 wenzelm prove_common: include all sorts from context into statement, check shyps of result;
Wed, 01 Oct 2008 12:18:18 +0200 wenzelm renamed promise to future, tuned related interfaces;
Thu, 25 Sep 2008 20:34:18 +0200 wenzelm simplified Thm.promise;
Thu, 25 Sep 2008 14:35:01 +0200 wenzelm prove: error with original thread position;
Tue, 23 Sep 2008 23:07:48 +0200 wenzelm prove_multi: immediate;
Tue, 23 Sep 2008 22:04:30 +0200 wenzelm added promise_result, prove_promise;
Sat, 14 Jun 2008 23:20:11 +0200 wenzelm prove: full Variable.declare_term, including constraints;
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Thu, 17 Apr 2008 22:22:25 +0200 wenzelm prove_global: Variable.set_body true, pass context;
Sat, 12 Apr 2008 17:00:40 +0200 wenzelm replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
Mon, 05 Nov 2007 23:17:02 +0100 wenzelm removed unused compose_hhf, comp_hhf;
Tue, 03 Jul 2007 17:17:11 +0200 wenzelm moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
Tue, 19 Jun 2007 23:15:27 +0200 wenzelm balanced conjunctions;
Mon, 18 Jun 2007 23:30:46 +0200 wenzelm tuned conjunction tactics: slightly smaller proof terms;
Wed, 13 Jun 2007 00:01:59 +0200 wenzelm renamed prove_raw to prove_internal;
Mon, 04 Jun 2007 21:04:19 +0200 wenzelm added assume_rule_tac;
Thu, 10 May 2007 00:39:48 +0200 wenzelm moved some Drule operations to Thm (see more_thm.ML);
Thu, 07 Dec 2006 00:42:04 +0100 wenzelm reorganized structure Goal vs. Tactic;
Thu, 30 Nov 2006 14:17:29 +0100 wenzelm added norm/close_result (supercede local_standard etc.);
Wed, 29 Nov 2006 04:11:12 +0100 wenzelm COMP_INCR;
Fri, 24 Nov 2006 22:05:12 +0100 wenzelm ProofContext.init;
Wed, 02 Aug 2006 22:26:44 +0200 wenzelm normalized Proof.context/method type aliases;
Sun, 30 Jul 2006 21:28:52 +0200 wenzelm Thm.adjust_maxidx;
Sat, 29 Jul 2006 00:51:32 +0200 wenzelm prove: proper assumption context, more tactic arguments;
Thu, 27 Jul 2006 13:43:06 +0200 wenzelm moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
Wed, 19 Jul 2006 12:12:00 +0200 wenzelm prove: Variable.declare_internal (more efficient);
Sat, 08 Jul 2006 12:54:44 +0200 wenzelm prove/prove_multi: context;
Mon, 12 Jun 2006 21:19:02 +0200 wenzelm Unify.matches_list;
Mon, 05 Jun 2006 21:54:20 +0200 wenzelm allow non-trivial schematic goals (via embedded term vars);
Thu, 11 May 2006 21:46:17 +0200 wenzelm check result against certified prop, i.e. admit non-normal statements;
Thu, 27 Apr 2006 15:06:35 +0200 wenzelm tuned basic list operators (flat, maps, map_filter);
Thu, 13 Apr 2006 12:01:01 +0200 wenzelm use conjunction stuff from conjunction.ML;
Wed, 08 Mar 2006 18:37:27 +0100 wenzelm tuned;
Sun, 05 Mar 2006 23:56:57 +0100 wenzelm SELECT_GOAL: fixed trivial case;
Sat, 04 Mar 2006 21:10:08 +0100 wenzelm added extract, retrofit;
Sat, 14 Jan 2006 17:14:06 +0100 wenzelm sane ERROR handling;
less more (0) -60 tip