| 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
|
| Fri, 19 Jan 2007 13:09:32 +0100 |
wenzelm |
ML context: full generic context, tuned signature;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2006 16:08:00 +0100 |
wenzelm |
removed conditional combinator;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 22:14:45 +0100 |
wenzelm |
added mapping_result;
|
file |
diff |
annotate
|
| Fri, 24 Nov 2006 22:05:14 +0100 |
wenzelm |
fake predeclaration of structure ProofContext;
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 19:37:05 +0200 |
wenzelm |
moved Context.ml_output to Output.ml_output;
|
file |
diff |
annotate
|
| Sun, 01 Oct 2006 22:19:24 +0200 |
wenzelm |
exists_name: include this theory name;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:51 +0200 |
wenzelm |
fake predeclaration of type Proof.context;
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 16:53:31 +0200 |
haftmann |
fixed typo
|
file |
diff |
annotate
|
| Wed, 17 May 2006 22:34:47 +0200 |
wenzelm |
added mapping;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:34:55 +0100 |
wenzelm |
removed distinct, renamed gen_distinct to distinct;
|
file |
diff |
annotate
|
| Sun, 12 Feb 2006 21:34:22 +0100 |
wenzelm |
structure Datatab: private copy avoids potential conflict of table exceptions;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:58:57 +0100 |
wenzelm |
TableFun: renamed xxx_multi to xxx_list;
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:23 +0100 |
wenzelm |
rename map_theory/proof to theory/proof_map;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:16 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|