| Sat, 06 Dec 2008 00:08:07 +0100 |
wenzelm |
finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 22:44:26 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 26 Sep 2008 19:07:56 +0200 |
wenzelm |
eliminated polymorphic equality;
|
file |
diff |
annotate
|
| Mon, 22 Sep 2008 15:26:11 +0200 |
wenzelm |
added reject_draft;
|
file |
diff |
annotate
|
| Thu, 04 Sep 2008 16:03:44 +0200 |
wenzelm |
Thread.getLocal/setLocal;
|
file |
diff |
annotate
|
| Tue, 24 Jun 2008 19:43:17 +0200 |
wenzelm |
added pprint_thy_ref;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 17:03:20 +0200 |
wenzelm |
eliminated theory CPure;
|
file |
diff |
annotate
|
| Wed, 14 May 2008 14:43:37 +0200 |
wenzelm |
names_of: exclude intermediate ids -- less verbosity;
|
file |
diff |
annotate
|
| Thu, 10 Apr 2008 20:54:15 +0200 |
wenzelm |
export is_draft, not draftN;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 19:14:08 +0100 |
wenzelm |
added map_theory_result, map_proof_result;
|
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
|
| Thu, 27 Mar 2008 14:41:14 +0100 |
wenzelm |
eliminated theory ProtoPure;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 12:06:26 +0100 |
wenzelm |
nonfix >>;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2008 22:40:03 +0100 |
wenzelm |
added thread data (formerly global ref in ML/ml_context.ML);
|
file |
diff |
annotate
|
| Sat, 08 Sep 2007 19:58:35 +0200 |
wenzelm |
removed thy_ord (erratic due to multi-threading);
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 23:41:35 +0200 |
wenzelm |
tuned CRITICAL sections;
|
file |
diff |
annotate
|
| Wed, 08 Aug 2007 16:40:20 +0200 |
wenzelm |
thread-safeness: when creating certified items, perform Theory.check_thy *last*;
|
file |
diff |
annotate
|
| Fri, 03 Aug 2007 16:28:20 +0200 |
wenzelm |
improved check_thy: produce a checked theory_ref (thread-safe version);
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 20:47:56 +0200 |
wenzelm |
marked some CRITICAL sections;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 20:01:32 +0200 |
wenzelm |
the_theory/proof: error instead of exception Fail;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 00:01:58 +0200 |
wenzelm |
merge/merge_refs: plain error instead of exception TERM;
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:50:09 +0200 |
wenzelm |
simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
|
file |
diff |
annotate
|
| Mon, 30 Apr 2007 13:33:00 +0200 |
wenzelm |
removed obsolete get_sg;
|
file |
diff |
annotate
|
| Thu, 05 Apr 2007 00:30:31 +0200 |
wenzelm |
added thy_ord -- order of creation;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 23:29:39 +0200 |
wenzelm |
theory: maintain ancestors in order of creation;
|
file |
diff |
annotate
|
| Sun, 21 Jan 2007 16:46:06 +0100 |
wenzelm |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
|
file |
diff |
annotate
|
| Sun, 21 Jan 2007 16:43:47 +0100 |
wenzelm |
tuned comments
|
file |
diff |
annotate
|
| Sat, 20 Jan 2007 14:09:16 +0100 |
wenzelm |
added is_finished_thy;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:02 +0100 |
wenzelm |
moved ML context stuff to from Context to ML_Context;
|
file |
diff |
annotate
|