| 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
|
| Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2006 01:13:02 +0100 |
wenzelm |
added map_theory, map_proof;
|
file |
diff |
annotate
|
| Tue, 10 Jan 2006 19:33:31 +0100 |
wenzelm |
support for generic contexts with data;
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 19:01:37 +0200 |
wenzelm |
minor tweaks for Poplog/ML;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:16:56 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
| Tue, 13 Sep 2005 22:19:24 +0200 |
wenzelm |
replaced DATA_FAIL by EXCEPTION;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2005 18:48:50 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 13:42:31 +0200 |
wenzelm |
type proof: theory_ref instead of theory (make proof contexts independent entities);
|
file |
diff |
annotate
|
| Tue, 19 Jul 2005 20:47:01 +0200 |
wenzelm |
Inttab.defined;
|
file |
diff |
annotate
|
| Wed, 06 Jul 2005 20:00:24 +0200 |
wenzelm |
check_thy: less invocations, less verbose;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2005 15:13:23 +0200 |
wenzelm |
added joinable;
|
file |
diff |
annotate
|
| Wed, 22 Jun 2005 19:41:18 +0200 |
wenzelm |
begin_thy: merge maximal imports;
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 22:14:03 +0200 |
wenzelm |
improved treatment of intermediate checkpoints: actual copy
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:33:21 +0200 |
wenzelm |
added type theory: generic theory contexts with unique identity,
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 22:02:06 +0200 |
wenzelm |
superceded by Pure.thy and CPure.thy;
|
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
|
| Sun, 20 Jun 2004 09:27:24 +0200 |
wenzelm |
use_output: Symbol.escape;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2001 18:52:30 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2001 21:54:43 +0100 |
wenzelm |
use_output: proper handling of non-ASCII symbols;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2001 00:35:50 +0100 |
wenzelm |
use_text etc.: proper output of error messages;
|
file |
diff |
annotate
|
| Fri, 12 Jan 2001 20:04:22 +0100 |
wenzelm |
use_mltext: priority output;
|
file |
diff |
annotate
|
| Mon, 14 Aug 2000 14:49:49 +0200 |
wenzelm |
use_let: exclude 'val';
|
file |
diff |
annotate
|
| Fri, 05 May 2000 21:57:58 +0200 |
wenzelm |
tuned msg;
|
file |
diff |
annotate
|
| Mon, 06 Mar 2000 21:08:15 +0100 |
wenzelm |
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
|
file |
diff |
annotate
|
| Tue, 09 Mar 1999 12:05:07 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 08 Feb 1999 17:31:50 +0100 |
wenzelm |
added fetch, fetch_theory;
|
file |
diff |
annotate
|
| Fri, 05 Feb 1999 20:57:18 +0100 |
wenzelm |
setmp: theory option;
|
file |
diff |
annotate
|
| Wed, 03 Feb 1999 16:40:42 +0100 |
wenzelm |
Global theory context (used to be in Thy/context.ML);
|
file |
diff |
annotate
|