| Tue, 05 Oct 1999 15:24:58 +0200 |
berghofe |
Rule not_not is now stored in theory (needed by Inductive).
|
changeset |
files
|
| Tue, 05 Oct 1999 15:23:22 +0200 |
berghofe |
Monotonicity rules for inductive definitions can now be added to a theory via
|
changeset |
files
|
| Tue, 05 Oct 1999 14:11:34 +0200 |
wenzelm |
macros for Isabelle generated LaTeX output;
|
changeset |
files
|
| Mon, 04 Oct 1999 21:48:59 +0200 |
wenzelm |
arithmetic now in IntArith;
|
changeset |
files
|
| Mon, 04 Oct 1999 21:48:23 +0200 |
wenzelm |
simprocs now in IntArith;
|
changeset |
files
|
| Mon, 04 Oct 1999 21:47:16 +0200 |
wenzelm |
IntArith;
|
changeset |
files
|
| Mon, 04 Oct 1999 21:46:49 +0200 |
wenzelm |
Tools/typedef_package.ML;
|
changeset |
files
|
| Mon, 04 Oct 1999 21:46:13 +0200 |
wenzelm |
eliminated ap/app;
|
changeset |
files
|
| Mon, 04 Oct 1999 21:45:10 +0200 |
wenzelm |
proper dependencies of all theories and packages;
|
changeset |
files
|
| Mon, 04 Oct 1999 21:44:28 +0200 |
wenzelm |
removed DatatypePackage.setup;
|
changeset |
files
|
| 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
|