| Thu, 05 Jun 1997 17:19:05 +0200 |
nipkow |
Moved image_is_empty from Finite.ML to equalities.ML
|
changeset |
files
|
| Thu, 05 Jun 1997 14:40:35 +0200 |
nipkow |
Modified a few defs and proofs because of the changes to theory Finite.thy.
|
changeset |
files
|
| Thu, 05 Jun 1997 14:39:22 +0200 |
nipkow |
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
|
changeset |
files
|
| Thu, 05 Jun 1997 14:06:23 +0200 |
paulson |
New recdef examples
|
changeset |
files
|
| Thu, 05 Jun 1997 13:55:29 +0200 |
paulson |
Removal of freeze_vars and thaw_vars. New freeze_thaw
|
changeset |
files
|
| Thu, 05 Jun 1997 13:53:59 +0200 |
paulson |
freezeT now refers to Type.freeze_thaw
|
changeset |
files
|
| Thu, 05 Jun 1997 13:52:43 +0200 |
paulson |
Tidying of signature. More robust renaming in freeze_thaw.
|
changeset |
files
|
| Thu, 05 Jun 1997 13:30:24 +0200 |
paulson |
Removal of freeze_vars and thaw_vars (quite unused...)
|
changeset |
files
|
| Thu, 05 Jun 1997 13:29:41 +0200 |
paulson |
Removal of radixstring from string_of_int; addition of string_of_indexname
|
changeset |
files
|
| Thu, 05 Jun 1997 13:28:32 +0200 |
paulson |
There was never need for another copy of radixstring...
|
changeset |
files
|
| Thu, 05 Jun 1997 13:27:28 +0200 |
paulson |
Numerous simplifications and removal of HOL-isms
|
changeset |
files
|
| Thu, 05 Jun 1997 13:26:09 +0200 |
paulson |
Now loads theory Recdef
|
changeset |
files
|