| 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
|
| Fri, 12 Dec 2008 12:14:02 +0100 |
wenzelm |
future proofs: more robust check via Future.enabled;
|
file |
diff |
annotate
|
| Thu, 09 Oct 2008 20:53:21 +0200 |
wenzelm |
moved future_scheduler flag to Concurrent/ROOT.ML;
|
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:20 +0200 |
wenzelm |
added future_scheduler (from thy_info.ML);
|
file |
diff |
annotate
|
| Thu, 18 Sep 2008 19:39:44 +0200 |
wenzelm |
simplified oracle interface;
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 22:22:21 +0200 |
wenzelm |
prove_global: pass context;
|
file |
diff |
annotate
|
| Thu, 03 Apr 2008 17:43:01 +0200 |
berghofe |
Added prove_global.
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 20:02:04 +0100 |
wenzelm |
Context.>> : operate on Context.generic;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 15:32:15 +0100 |
wenzelm |
eliminated delayed theory setup
|
file |
diff |
annotate
|
| Fri, 31 Aug 2007 18:46:37 +0200 |
wenzelm |
prove: setmp quick_and_dirty (avoids race condition);
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:41 +0200 |
wenzelm |
normalized Proof.context/method type aliases;
|
file |
diff |
annotate
|
| Sat, 29 Jul 2006 00:51:29 +0200 |
wenzelm |
Goal.prove: more tactic arguments;
|
file |
diff |
annotate
|
| Sat, 08 Jul 2006 12:54:37 +0200 |
wenzelm |
Goal.prove: context;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:34 +0200 |
wenzelm |
Goal.prove;
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 19:17:35 +0200 |
wenzelm |
moved quick_and_dirty to Pure/ROOT.ML;
|
file |
diff |
annotate
|
| Tue, 13 Sep 2005 22:19:47 +0200 |
wenzelm |
load before proof.ML;
|
file |
diff |
annotate
|
| Thu, 18 Aug 2005 11:17:49 +0200 |
wenzelm |
accomodate interface Proof vs. Method;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 23 Apr 2005 19:51:04 +0200 |
wenzelm |
qualified name Pure.skip_proof;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 22:02:06 +0200 |
wenzelm |
superceded by Pure.thy and CPure.thy;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2005 09:26:55 +0200 |
wenzelm |
Thm.invoke_oracle_i;
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Wed, 28 Nov 2001 23:31:47 +0100 |
wenzelm |
skip_proof: do not require quick_and_dirty in interactive mode;
|
file |
diff |
annotate
|
| Mon, 19 Nov 2001 23:37:01 +0100 |
wenzelm |
improved treatment of common result name;
|
file |
diff |
annotate
|
| Sun, 11 Nov 2001 21:37:44 +0100 |
wenzelm |
adapted to multiple results;
|
file |
diff |
annotate
|
| Mon, 05 Nov 2001 20:59:35 +0100 |
wenzelm |
pretty/print functions with context;
|
file |
diff |
annotate
|
| Sat, 27 Oct 2001 23:19:55 +0200 |
wenzelm |
added prove;
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 18:03:49 +0200 |
wenzelm |
moved prove_goalw_cterm to goals.ML;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2001 12:09:38 +0200 |
wenzelm |
added make_thm (sort-of);
|
file |
diff |
annotate
|
| Fri, 05 May 2000 22:09:41 +0200 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Mon, 20 Mar 2000 18:48:12 +0100 |
wenzelm |
added prove_goalw_cterm;
|
file |
diff |
annotate
|
| Mon, 12 Jul 1999 22:28:56 +0200 |
wenzelm |
local qed; print rule;
|
file |
diff |
annotate
|
| Thu, 08 Jul 1999 18:36:09 +0200 |
wenzelm |
propp: 'concl' patterns;
|
file |
diff |
annotate
|
| Fri, 02 Jul 1999 19:04:32 +0200 |
wenzelm |
skip_proof feature 'sorry' (for quick_and_dirty mode only);
|
file |
diff |
annotate
|