| Thu, 12 Mar 2009 15:54:58 +0100 |
wenzelm |
Assumption.all_prems_of, Assumption.all_assms_of;
|
file |
diff |
annotate
|
| Sun, 11 Jan 2009 18:18:35 +0100 |
wenzelm |
added Goal.future_enabled abstraction -- now also checks that this is already
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 04 Jan 2009 15:28:40 +0100 |
wenzelm |
tuned protect, conclude: Drule.comp_no_flatten;
|
file |
diff |
annotate
|
| Sun, 04 Jan 2009 00:01:16 +0100 |
wenzelm |
future proofs: back to Future.fork_pri ~1 for improved parallelism;
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 18:04:16 +0100 |
wenzelm |
future proofs: Future.fork_pri 1 minimizes queue length and pending promises
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 16:25:19 +0100 |
wenzelm |
Future.fork_pri;
|
file |
diff |
annotate
|
| Fri, 12 Dec 2008 12:14:02 +0100 |
wenzelm |
future proofs: more robust check via Future.enabled;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 23:00:58 +0100 |
wenzelm |
future proofs: pass actual futures to facilitate composite computations;
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 22:44:28 +0200 |
wenzelm |
prove_common: include all sorts from context into statement, check shyps of result;
|
file |
diff |
annotate
|
| Wed, 01 Oct 2008 12:18:18 +0200 |
wenzelm |
renamed promise to future, tuned related interfaces;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 20:34:18 +0200 |
wenzelm |
simplified Thm.promise;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 14:35:01 +0200 |
wenzelm |
prove: error with original thread position;
|
file |
diff |
annotate
|
| Tue, 23 Sep 2008 23:07:48 +0200 |
wenzelm |
prove_multi: immediate;
|
file |
diff |
annotate
|
| Tue, 23 Sep 2008 22:04:30 +0200 |
wenzelm |
added promise_result, prove_promise;
|
file |
diff |
annotate
|
| Sat, 14 Jun 2008 23:20:11 +0200 |
wenzelm |
prove: full Variable.declare_term, including constraints;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 22:22:25 +0200 |
wenzelm |
prove_global: Variable.set_body true, pass context;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:40 +0200 |
wenzelm |
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 23:17:02 +0100 |
wenzelm |
removed unused compose_hhf, comp_hhf;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Tue, 19 Jun 2007 23:15:27 +0200 |
wenzelm |
balanced conjunctions;
|
file |
diff |
annotate
|
| Mon, 18 Jun 2007 23:30:46 +0200 |
wenzelm |
tuned conjunction tactics: slightly smaller proof terms;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 00:01:59 +0200 |
wenzelm |
renamed prove_raw to prove_internal;
|
file |
diff |
annotate
|
| Mon, 04 Jun 2007 21:04:19 +0200 |
wenzelm |
added assume_rule_tac;
|
file |
diff |
annotate
|
| Thu, 10 May 2007 00:39:48 +0200 |
wenzelm |
moved some Drule operations to Thm (see more_thm.ML);
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 00:42:04 +0100 |
wenzelm |
reorganized structure Goal vs. Tactic;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 14:17:29 +0100 |
wenzelm |
added norm/close_result (supercede local_standard etc.);
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 04:11:12 +0100 |
wenzelm |
COMP_INCR;
|
file |
diff |
annotate
|
| Fri, 24 Nov 2006 22:05:12 +0100 |
wenzelm |
ProofContext.init;
|
file |
diff |
annotate
|