| Mon, 30 Sep 1996 11:10:22 +0200 |
paulson |
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
|
changeset |
files
|
| Mon, 30 Sep 1996 11:04:14 +0200 |
paulson |
Improved discussion of shyps thanks to Markus Wenzel
|
changeset |
files
|
| Mon, 30 Sep 1996 10:59:47 +0200 |
paulson |
prune_params_tac no longer rewrites main goal
|
changeset |
files
|
| Thu, 26 Sep 1996 17:34:36 +0200 |
paulson |
Added catch-all clause to drop, preventing exception Match
|
changeset |
files
|
| Thu, 26 Sep 1996 17:30:52 +0200 |
paulson |
Now replaces uses of ssubst by stac
|
changeset |
files
|
| Thu, 26 Sep 1996 17:15:19 +0200 |
paulson |
Documented sort hypotheses and improved discussion of derivations
|
changeset |
files
|
| Thu, 26 Sep 1996 17:14:02 +0200 |
paulson |
Documented defer_tac and moved back the obsolete tactics like fold_tac
|
changeset |
files
|
| Thu, 26 Sep 1996 17:13:18 +0200 |
paulson |
Documented stac, and updated the documentation of hyp_subst_tac
|
changeset |
files
|
| Thu, 26 Sep 1996 17:02:51 +0200 |
paulson |
Declared stac
|
changeset |
files
|
| Thu, 26 Sep 1996 16:38:02 +0200 |
paulson |
Ran expandshort; used stac instead of ssubst
|
changeset |
files
|
| Thu, 26 Sep 1996 16:12:25 +0200 |
paulson |
Ran expandshort; used stac instead of ssubst
|
changeset |
files
|
| Thu, 26 Sep 1996 15:49:54 +0200 |
paulson |
Ran expandshort; used stac instead of ssubst
|
changeset |
files
|
| Thu, 26 Sep 1996 15:14:23 +0200 |
paulson |
Ran expandshort; used stac instead of ssubst
|
changeset |
files
|
| Thu, 26 Sep 1996 12:50:48 +0200 |
paulson |
Introduction of "lost" argument
|
changeset |
files
|
| Thu, 26 Sep 1996 12:47:47 +0200 |
paulson |
Ran expandshort
|
changeset |
files
|
| Thu, 26 Sep 1996 11:11:22 +0200 |
paulson |
Changed freeze to freeze_thaw
|
changeset |
files
|
| Thu, 26 Sep 1996 11:10:46 +0200 |
paulson |
Generalized freeze to freeze_thaw in order to
|
changeset |
files
|
| Thu, 26 Sep 1996 10:34:19 +0200 |
paulson |
Last working version prior to addition of "lost" component
|
changeset |
files
|
| Wed, 25 Sep 1996 18:01:18 +0200 |
paulson |
Last working version before "lost"
|
changeset |
files
|
| Wed, 25 Sep 1996 17:15:18 +0200 |
paulson |
Last working version prior to introduction of "lost"
|
changeset |
files
|
| Wed, 25 Sep 1996 15:03:13 +0200 |
paulson |
Prevention of Overflow exception (for SML/NJ) in gensym
|
changeset |
files
|
| Wed, 25 Sep 1996 11:14:18 +0200 |
paulson |
Rationalized the rewriting of membership for {} and insert
|
changeset |
files
|
| Wed, 25 Sep 1996 11:10:31 +0200 |
paulson |
Calls discgarb -c to realize dramatic space savings!
|
changeset |
files
|
| Tue, 24 Sep 1996 13:54:27 +0200 |
paulson |
Fixed spelling error in comment
|
changeset |
files
|
| Tue, 24 Sep 1996 13:53:18 +0200 |
paulson |
Added miniscoping for UN and INT
|
changeset |
files
|
| Tue, 24 Sep 1996 13:51:10 +0200 |
paulson |
Restoration of reference to Nipkow, LICS, 1993
|
changeset |
files
|
| Tue, 24 Sep 1996 09:02:34 +0200 |
nipkow |
Moved Option out of IOA into core HOL
|
changeset |
files
|
| Tue, 24 Sep 1996 08:59:24 +0200 |
nipkow |
Moved Option into core HOL which caused a few local changes.
|
changeset |
files
|