| Thu, 16 Oct 1997 14:12:58 +0200 |
nipkow |
Simplified proof because of better simplifier.
|
changeset |
files
|
| Thu, 16 Oct 1997 14:12:15 +0200 |
nipkow |
Various new lemmas. Improved conversion of equations to rewrite rules:
|
changeset |
files
|
| Thu, 16 Oct 1997 14:00:20 +0200 |
wenzelm |
added transfer: theory -> thm -> thm;
|
changeset |
files
|
| Thu, 16 Oct 1997 13:45:27 +0200 |
wenzelm |
oops;
|
changeset |
files
|
| Thu, 16 Oct 1997 13:45:16 +0200 |
nipkow |
The simplifier has been improved a little: equations s=t which used to be
|
changeset |
files
|
| Thu, 16 Oct 1997 13:43:42 +0200 |
wenzelm |
fixed dependencies;
|
changeset |
files
|
| Thu, 16 Oct 1997 13:42:53 +0200 |
wenzelm |
transfer thy Ord_nat;
|
changeset |
files
|
| Thu, 16 Oct 1997 13:42:29 +0200 |
wenzelm |
sevaral goals restated in mono.thy;
|
changeset |
files
|
| Thu, 16 Oct 1997 13:39:20 +0200 |
wenzelm |
moved rank_Inl, rank_Inr from Epsilon.ML to Univ.ML;
|
changeset |
files
|
| Thu, 16 Oct 1997 13:38:47 +0200 |
wenzelm |
transfer InfDatatype.thy Limit_VfromE;
|
changeset |
files
|
| Thu, 16 Oct 1997 13:38:28 +0200 |
wenzelm |
transfer CardinalArith.thy nat_into_Ord;
|
changeset |
files
|
| Thu, 16 Oct 1997 13:36:04 +0200 |
wenzelm |
improved pretty_arity;
|
changeset |
files
|
| Thu, 16 Oct 1997 13:34:15 +0200 |
wenzelm |
added merge_theories (new name arg);
|
changeset |
files
|
| Thu, 16 Oct 1997 13:33:17 +0200 |
wenzelm |
fixed merge_theories;
|
changeset |
files
|