Thu, 18 Feb 2010 10:01:48 +0100 |
Cezary Kaliszyk |
Changed back to original version of trm5
|
changeset |
files
|
Thu, 18 Feb 2010 10:00:58 +0100 |
Cezary Kaliszyk |
The alternate version of trm5 with additional binding. All proofs work the same.
|
changeset |
files
|
Thu, 18 Feb 2010 09:46:38 +0100 |
Cezary Kaliszyk |
Code for handling atom sets.
|
changeset |
files
|
Thu, 18 Feb 2010 08:43:13 +0100 |
Cezary Kaliszyk |
Replace Terms by Terms2.
|
changeset |
files
|
Thu, 18 Feb 2010 08:37:45 +0100 |
Cezary Kaliszyk |
Fixed proofs in Terms2 and found a mistake in Terms.
|
changeset |
files
|
Wed, 17 Feb 2010 17:51:35 +0100 |
Cezary Kaliszyk |
Terms2 with bindings for binders synchronized with bindings they are used in.
|
changeset |
files
|
Wed, 17 Feb 2010 17:29:26 +0100 |
Cezary Kaliszyk |
Cleaning of proofs in Terms.
|
changeset |
files
|
Wed, 17 Feb 2010 16:22:16 +0100 |
Cezary Kaliszyk |
Testing Fv
|
changeset |
files
|
Wed, 17 Feb 2010 15:52:08 +0100 |
Cezary Kaliszyk |
Fix the strong induction principle.
|
changeset |
files
|
Wed, 17 Feb 2010 15:45:03 +0100 |
Cezary Kaliszyk |
Reorder
|
changeset |
files
|
Wed, 17 Feb 2010 15:28:50 +0100 |
Cezary Kaliszyk |
Add bindings of recursive types by free_variables.
|
changeset |
files
|
Wed, 17 Feb 2010 15:20:22 +0100 |
Cezary Kaliszyk |
Bindings adapted to multiple defined datatypes.
|
changeset |
files
|
Wed, 17 Feb 2010 15:00:04 +0100 |
Cezary Kaliszyk |
Reorganization
|
changeset |
files
|
Wed, 17 Feb 2010 14:44:32 +0100 |
Cezary Kaliszyk |
Now should work.
|
changeset |
files
|
Wed, 17 Feb 2010 14:35:06 +0100 |
Cezary Kaliszyk |
Some optimizations and fixes.
|
changeset |
files
|