| Fri, 06 Sep 1996 11:56:12 +0200 |
paulson |
Improved error handling: if there are syntax or type-checking
|
changeset |
files
|
| Fri, 06 Sep 1996 10:45:48 +0200 |
paulson |
Modified proof to work with miniscoping
|
changeset |
files
|
| Thu, 05 Sep 1996 18:42:48 +0200 |
paulson |
Now uses thin_tac
|
changeset |
files
|
| Thu, 05 Sep 1996 18:31:14 +0200 |
paulson |
Now uses thin_tac
|
changeset |
files
|
| Thu, 05 Sep 1996 18:30:13 +0200 |
paulson |
Renaming of _rews to _simps
|
changeset |
files
|
| Thu, 05 Sep 1996 18:29:43 +0200 |
paulson |
Added thin_tac to signature; previous change was useless
|
changeset |
files
|
| Thu, 05 Sep 1996 18:28:54 +0200 |
paulson |
Some renaming. Note that this miniscoping is more
|
changeset |
files
|
| Thu, 05 Sep 1996 18:28:01 +0200 |
paulson |
Introduction of miniscoping for FOL
|
changeset |
files
|
| Thu, 05 Sep 1996 10:30:42 +0200 |
paulson |
Pretty-printing change to emphasize the scope of assumptions
|
changeset |
files
|
| Thu, 05 Sep 1996 10:29:52 +0200 |
paulson |
Declared thin_tac
|
changeset |
files
|
| Thu, 05 Sep 1996 10:29:20 +0200 |
paulson |
Miniscoping rules are deleted, as these brittle proofs
|
changeset |
files
|
| Thu, 05 Sep 1996 10:27:36 +0200 |
paulson |
Simplified some proofs for compatibility with miniscoping
|
changeset |
files
|
| Thu, 05 Sep 1996 10:23:55 +0200 |
paulson |
Added miniscoping to the simplifier: quantifiers are now pushed in
|
changeset |
files
|
| Tue, 03 Sep 1996 19:07:23 +0200 |
paulson |
Fixed pretty-printing of {|...|}
|
changeset |
files
|
| Tue, 03 Sep 1996 19:07:00 +0200 |
paulson |
New theorems for Fake case
|
changeset |
files
|