Mon, 04 Oct 1999 21:44:07 +0200 |
wenzelm |
load / setup recdef package (TFL);
|
changeset |
files
|
Mon, 04 Oct 1999 21:43:45 +0200 |
wenzelm |
load / setup datatype package;
|
changeset |
files
|
Mon, 04 Oct 1999 21:43:05 +0200 |
wenzelm |
removed TFL/sys.sml;
|
changeset |
files
|
Mon, 04 Oct 1999 21:41:19 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
Mon, 04 Oct 1999 21:41:09 +0200 |
wenzelm |
renamed 'prefix' to 'prfx' (avoids clash with infix);
|
changeset |
files
|
Mon, 04 Oct 1999 21:39:36 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 04 Oct 1999 21:39:10 +0200 |
wenzelm |
mk_frees, assume_read moved here;
|
changeset |
files
|
Mon, 04 Oct 1999 21:37:35 +0200 |
wenzelm |
tryres, gen_make_elim moved here;
|
changeset |
files
|
Mon, 04 Oct 1999 21:37:00 +0200 |
wenzelm |
FOLogic.mk_conj;
|
changeset |
files
|
Mon, 04 Oct 1999 21:35:26 +0200 |
wenzelm |
added mk_conj, mk_disj, mk_imp;
|
changeset |
files
|
Mon, 04 Oct 1999 21:34:20 +0200 |
wenzelm |
added BVC;
|
changeset |
files
|
Mon, 04 Oct 1999 14:45:35 +0200 |
wenzelm |
added mk_conj, mk_disj, mk_imp;
|
changeset |
files
|
Mon, 04 Oct 1999 13:47:28 +0200 |
paulson |
working snapshot (even Alloc)
|
changeset |
files
|
Mon, 04 Oct 1999 13:45:31 +0200 |
paulson |
most results now refer to those for "extend"
|
changeset |
files
|
Mon, 04 Oct 1999 12:22:14 +0200 |
wenzelm |
fixed lookup_theory;
|
changeset |
files
|
Mon, 04 Oct 1999 10:19:18 +0200 |
paulson |
fixed CHANGED_GOAL, which is used by stac
|
changeset |
files
|
Sun, 03 Oct 1999 15:54:25 +0200 |
wenzelm |
improved theory_source presentation (hook);
|
changeset |
files
|
Sun, 03 Oct 1999 15:54:04 +0200 |
wenzelm |
improved theory_source presentation;
|
changeset |
files
|
Sun, 03 Oct 1999 15:52:53 +0200 |
wenzelm |
export token_source;
|
changeset |
files
|
Sun, 03 Oct 1999 15:51:38 +0200 |
wenzelm |
added Space, Comment token kinds (keep actual text);
|
changeset |
files
|
Fri, 01 Oct 1999 20:41:58 +0200 |
wenzelm |
fixed no_qed;
|
changeset |
files
|
Fri, 01 Oct 1999 20:40:03 +0200 |
wenzelm |
added Isar/obtain.ML;
|
changeset |
files
|
Fri, 01 Oct 1999 20:39:40 +0200 |
wenzelm |
improved 'fix' / Skolem interfaces;
|
changeset |
files
|
Fri, 01 Oct 1999 20:38:50 +0200 |
wenzelm |
added 'obtain' command;
|
changeset |
files
|
Fri, 01 Oct 1999 20:38:16 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
Fri, 01 Oct 1999 20:38:00 +0200 |
wenzelm |
added prf_asm_goal;
|
changeset |
files
|
Fri, 01 Oct 1999 20:37:38 +0200 |
wenzelm |
added atomic_thesis;
|
changeset |
files
|
Fri, 01 Oct 1999 20:36:53 +0200 |
wenzelm |
The 'obtain' language element -- achieves (eliminated) existential
|
changeset |
files
|
Fri, 01 Oct 1999 18:36:12 +0200 |
wenzelm |
added undef_global_attribute, undef_local_attribute;
|
changeset |
files
|
Fri, 01 Oct 1999 10:23:13 +0200 |
berghofe |
- Fixed bug in mk_split_pack which caused application of expansion theorem
|
changeset |
files
|