| Sat, 25 Jul 2009 10:31:27 +0200 |
wenzelm |
renamed structure Display_Goal to Goal_Display;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 16:52:16 +0200 |
wenzelm |
clarified pretty_goals, pretty_thm_aux: plain context;
|
file |
diff |
annotate
|
| Mon, 20 Jul 2009 21:20:09 +0200 |
wenzelm |
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
|
file |
diff |
annotate
|
| Mon, 20 Jul 2009 00:37:39 +0200 |
wenzelm |
Proof.future_proof: declare all assumptions as well;
|
file |
diff |
annotate
|
| Sun, 19 Jul 2009 19:24:04 +0200 |
wenzelm |
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
|
file |
diff |
annotate
|
| Sun, 19 Jul 2009 18:02:40 +0200 |
wenzelm |
more abstract Future.is_worker;
|
file |
diff |
annotate
|
| Sun, 19 Jul 2009 14:15:47 +0200 |
wenzelm |
future_result: explicitly impose Variable.sorts_of again;
|
file |
diff |
annotate
|
| 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
|