| Tue, 05 Oct 1999 15:26:10 +0200 |
wenzelm |
added position;
|
changeset |
files
|
| Tue, 05 Oct 1999 15:25:52 +0200 |
berghofe |
Additional rules for inductive package.
|
changeset |
files
|
| Tue, 05 Oct 1999 15:25:35 +0200 |
wenzelm |
added untabify;
|
changeset |
files
|
| 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
|