| Tue, 24 Jul 2007 19:44:39 +0200 |
wenzelm |
require_thy: explicit tasks graph;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 19:45:46 +0200 |
wenzelm |
marked some CRITICAL sections;
|
file |
diff |
annotate
|
| Sun, 22 Jul 2007 21:20:55 +0200 |
wenzelm |
added simultaneous use_thys;
|
file |
diff |
annotate
|
| Sun, 22 Jul 2007 13:53:52 +0200 |
wenzelm |
begin_theory: simplified interface, keep thy info empty until end_theory;
|
file |
diff |
annotate
|
| Sat, 21 Jul 2007 17:40:40 +0200 |
wenzelm |
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 17:54:17 +0200 |
wenzelm |
simplified ThyLoad interfaces: only one additional directory;
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 23:18:58 +0200 |
wenzelm |
removed obsolete use/update_thy_only;
|
file |
diff |
annotate
|
| Tue, 30 Jan 2007 13:16:58 +0100 |
aspinall |
Add get_succs
|
file |
diff |
annotate
|
| Sun, 21 Jan 2007 16:46:40 +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:22 +0100 |
wenzelm |
added @{theory};
|
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:33 +0100 |
wenzelm |
adapted ML context operations;
|
file |
diff |
annotate
|
| Fri, 15 Dec 2006 00:08:06 +0100 |
wenzelm |
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:04:20 +0200 |
wenzelm |
member (op =);
|
file |
diff |
annotate
|
| Tue, 02 May 2006 20:42:43 +0200 |
wenzelm |
added the_theory;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Wed, 26 Apr 2006 22:38:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 Mar 2006 12:18:15 +0100 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:26 +0100 |
wenzelm |
use/use_thy: Output.toplevel_errors;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 19:01:37 +0200 |
wenzelm |
minor tweaks for Poplog/ML;
|
file |
diff |
annotate
|
| Tue, 13 Sep 2005 22:19:50 +0200 |
wenzelm |
begin_theory: tuned interface, check uses;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 09:37:12 +0200 |
haftmann |
introduced AList.*
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 22:14:19 +0200 |
wenzelm |
Theory.begin/end_theory;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:33:39 +0200 |
wenzelm |
removed obsolete theory_of_sign, theory_of_thm;
|
file |
diff |
annotate
|
| Mon, 23 May 2005 14:56:37 +0200 |
wenzelm |
tuned pretty_sg;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 22:02:06 +0200 |
wenzelm |
superceded by Pure.thy and CPure.thy;
|
file |
diff |
annotate
|
| Sat, 26 Mar 2005 18:20:29 +0100 |
paulson |
new display of theory stamps
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|