Thu, 22 Nov 2001 17:13:36 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Thu, 22 Nov 2001 17:13:24 +0100 |
wenzelm |
thm "point.defs";
|
changeset |
files
|
Thu, 22 Nov 2001 17:13:06 +0100 |
wenzelm |
recovered original "make";
|
changeset |
files
|
Thu, 22 Nov 2001 17:12:08 +0100 |
wenzelm |
renamed "fields" to "flds" (avoid clash with new "fields" operation);
|
changeset |
files
|
Wed, 21 Nov 2001 20:20:18 +0100 |
wenzelm |
locale expressions;
|
changeset |
files
|
Wed, 21 Nov 2001 00:36:51 +0100 |
wenzelm |
use tracing function for trace output;
|
changeset |
files
|
Wed, 21 Nov 2001 00:35:13 +0100 |
wenzelm |
tracing_fn;
|
changeset |
files
|
Wed, 21 Nov 2001 00:34:38 +0100 |
wenzelm |
added tracing, tracing_fn;
|
changeset |
files
|
Wed, 21 Nov 2001 00:34:06 +0100 |
wenzelm |
Set.vimage;
|
changeset |
files
|
Wed, 21 Nov 2001 00:33:40 +0100 |
wenzelm |
got rid of theory Inverse_Image;
|
changeset |
files
|
Wed, 21 Nov 2001 00:33:04 +0100 |
wenzelm |
theory Inverse_Image converted and moved to Set;
|
changeset |
files
|
Wed, 21 Nov 2001 00:32:10 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 20 Nov 2001 22:54:06 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 20 Nov 2001 22:53:50 +0100 |
wenzelm |
fixed links etc.;
|
changeset |
files
|
Tue, 20 Nov 2001 22:53:05 +0100 |
wenzelm |
* HOL/record: cases/induct for more parts;
|
changeset |
files
|
Tue, 20 Nov 2001 20:57:46 +0100 |
wenzelm |
prefer later trfuns;
|
changeset |
files
|
Tue, 20 Nov 2001 20:57:07 +0100 |
wenzelm |
moved prefixes1, suffixes1 to library.ML;
|
changeset |
files
|
Tue, 20 Nov 2001 20:56:42 +0100 |
wenzelm |
trfuns *after* binder syntax;
|
changeset |
files
|
Tue, 20 Nov 2001 20:56:13 +0100 |
wenzelm |
added prefixes1, suffixes1;
|
changeset |
files
|
Tue, 20 Nov 2001 20:55:50 +0100 |
wenzelm |
print_depth 10;
|
changeset |
files
|
Tue, 20 Nov 2001 20:55:33 +0100 |
wenzelm |
derive cases/induct rules for ``more'' parts;
|
changeset |
files
|
Tue, 20 Nov 2001 20:54:12 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 20 Nov 2001 10:48:38 +0100 |
paulson |
Hyperreal
|
changeset |
files
|
Mon, 19 Nov 2001 23:37:01 +0100 |
wenzelm |
improved treatment of common result name;
|
changeset |
files
|
Mon, 19 Nov 2001 20:47:57 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 19 Nov 2001 20:47:39 +0100 |
wenzelm |
multi_theorem: common statement header (covers *all* results);
|
changeset |
files
|
Mon, 19 Nov 2001 20:46:38 +0100 |
wenzelm |
fixed comment;
|
changeset |
files
|
Mon, 19 Nov 2001 20:46:05 +0100 |
wenzelm |
induct method: localize rews for rule;
|
changeset |
files
|
Mon, 19 Nov 2001 17:42:00 +0100 |
berghofe |
Now handles different theorems with same name more gracefully.
|
changeset |
files
|
Mon, 19 Nov 2001 17:40:45 +0100 |
berghofe |
Improved error message.
|
changeset |
files
|
Mon, 19 Nov 2001 17:40:07 +0100 |
berghofe |
Added setup.
|
changeset |
files
|
Mon, 19 Nov 2001 17:39:31 +0100 |
berghofe |
Moved fastype to Envir.
|
changeset |
files
|