Mon, 23 Aug 1999 15:24:00 +0200 |
berghofe |
Moved sum_case to theory HOL/Datatype.
|
changeset |
files
|
Mon, 23 Aug 1999 11:43:21 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 23 Aug 1999 09:36:05 +0200 |
nipkow |
Corrected two busg in the simplifier.
|
changeset |
files
|
Sun, 22 Aug 1999 21:14:44 +0200 |
wenzelm |
\indexisarreg;
|
changeset |
files
|
Sun, 22 Aug 1999 21:14:28 +0200 |
wenzelm |
\VVar;
|
changeset |
files
|
Sun, 22 Aug 1999 21:13:20 +0200 |
wenzelm |
checkpoint;
|
changeset |
files
|
Sun, 22 Aug 1999 18:21:36 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 21 Aug 1999 16:59:03 +0200 |
wenzelm |
real numerals;
|
changeset |
files
|
Sat, 21 Aug 1999 16:54:09 +0200 |
wenzelm |
added HOL-Real;
|
changeset |
files
|
Fri, 20 Aug 1999 16:57:31 +0200 |
wenzelm |
echo ML_PLATFORM;
|
changeset |
files
|
Fri, 20 Aug 1999 16:16:16 +0200 |
wenzelm |
activate example;
|
changeset |
files
|
Fri, 20 Aug 1999 16:16:02 +0200 |
wenzelm |
delcongs [if_weak_cong];
|
changeset |
files
|
Fri, 20 Aug 1999 15:44:29 +0200 |
wenzelm |
print_context;
|
changeset |
files
|
Fri, 20 Aug 1999 15:43:25 +0200 |
wenzelm |
eliminated HOL-AxClasses target;
|
changeset |
files
|
Fri, 20 Aug 1999 15:42:46 +0200 |
wenzelm |
intro (no +);
|
changeset |
files
|
Fri, 20 Aug 1999 15:42:20 +0200 |
wenzelm |
mucke -res;
|
changeset |
files
|
Fri, 20 Aug 1999 15:41:53 +0200 |
wenzelm |
if_svc_enabled;
|
changeset |
files
|
Fri, 20 Aug 1999 15:41:19 +0200 |
wenzelm |
AxClasses, Isar_examples;
|
changeset |
files
|
Fri, 20 Aug 1999 15:34:51 +0200 |
wenzelm |
intro/elim: REPEAT1;
|
changeset |
files
|
Fri, 20 Aug 1999 11:54:32 +0200 |
paulson |
new theories RealBin, RealInt, RealPow
|
changeset |
files
|
Thu, 19 Aug 1999 22:00:33 +0200 |
wenzelm |
* HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with HOL/List;
|
changeset |
files
|
Thu, 19 Aug 1999 21:49:10 +0200 |
wenzelm |
quite a lot of tuning and cleanup;
|
changeset |
files
|
Thu, 19 Aug 1999 21:31:36 +0200 |
wenzelm |
sysman: Stefan Berghofer;
|
changeset |
files
|
Thu, 19 Aug 1999 20:05:13 +0200 |
wenzelm |
more;
|
changeset |
files
|
Thu, 19 Aug 1999 19:56:17 +0200 |
wenzelm |
Mucke, Einhoven;
|
changeset |
files
|
Thu, 19 Aug 1999 19:55:13 +0200 |
wenzelm |
quite a lot of tuning an cleanup;
|
changeset |
files
|
Thu, 19 Aug 1999 19:01:57 +0200 |
berghofe |
sum_case_Inl and sum_case_Inr are now defined in Datatype.ML.
|
changeset |
files
|
Thu, 19 Aug 1999 19:00:42 +0200 |
berghofe |
Moved sum_case stuff from Sum to Datatype.
|
changeset |
files
|
Thu, 19 Aug 1999 18:36:41 +0200 |
paulson |
real literals using binary arithmetic
|
changeset |
files
|
Thu, 19 Aug 1999 17:06:05 +0200 |
nipkow |
new entriues.
|
changeset |
files
|
Thu, 19 Aug 1999 16:54:38 +0200 |
paulson |
updated
|
changeset |
files
|
Thu, 19 Aug 1999 16:33:53 +0200 |
wenzelm |
disabled print_mode (tmp);
|
changeset |
files
|