| Thu, 28 Jan 2010 14:20:26 +0100 |
Christian Urban |
attempt to prove equivalence between alpha definitions
|
changeset |
files
|
| Thu, 28 Jan 2010 12:28:50 +0100 |
Cezary Kaliszyk |
End of renaming.
|
changeset |
files
|
| Thu, 28 Jan 2010 12:25:38 +0100 |
Cezary Kaliszyk |
Minor when looking at lam.distinct and lam.inject
|
changeset |
files
|
| Thu, 28 Jan 2010 12:24:49 +0100 |
Cezary Kaliszyk |
Renamed Bexeq to Bex1_rel
|
changeset |
files
|
| Thu, 28 Jan 2010 10:52:10 +0100 |
Cezary Kaliszyk |
Substracting bounds from free variables.
|
changeset |
files
|
| Thu, 28 Jan 2010 10:26:36 +0100 |
Cezary Kaliszyk |
Improper interface for datatype and function packages and proper interface lateron.
|
changeset |
files
|
| Thu, 28 Jan 2010 09:28:20 +0100 |
Christian Urban |
merged
|
changeset |
files
|
| Thu, 28 Jan 2010 09:28:06 +0100 |
Christian Urban |
minor
|
changeset |
files
|
| Thu, 28 Jan 2010 01:24:09 +0100 |
Christian Urban |
test about supp/freshness for lam (old proofs work in principle - for single binders)
|
changeset |
files
|
| Thu, 28 Jan 2010 08:13:39 +0100 |
Cezary Kaliszyk |
Recommited the changes for nitpick
|
changeset |
files
|
| Wed, 27 Jan 2010 18:26:01 +0100 |
Cezary Kaliszyk |
Correct types which fixes the printing.
|
changeset |
files
|
| Wed, 27 Jan 2010 18:06:14 +0100 |
Cezary Kaliszyk |
fv for subterms
|
changeset |
files
|
| Wed, 27 Jan 2010 17:39:13 +0100 |
Cezary Kaliszyk |
Fix the problem with later examples. Maybe need to go back to textual specifications.
|
changeset |
files
|
| Wed, 27 Jan 2010 17:18:30 +0100 |
Cezary Kaliszyk |
Some processing of variables in constructors to get free variables.
|
changeset |
files
|
| Wed, 27 Jan 2010 16:40:16 +0100 |
Cezary Kaliszyk |
Parsing of the input as terms and types, and passing them as such to the function package.
|
changeset |
files
|