Thu, 18 Feb 2010 15:03:09 +0100 |
Cezary Kaliszyk |
First (non-working) version of alpha-equivalence
|
changeset |
files
|
Thu, 18 Feb 2010 13:36:38 +0100 |
Cezary Kaliszyk |
Description of the fv procedure.
|
changeset |
files
|
Thu, 18 Feb 2010 12:06:59 +0100 |
Cezary Kaliszyk |
Testing auto constant lifting.
|
changeset |
files
|
Thu, 18 Feb 2010 11:28:20 +0100 |
Cezary Kaliszyk |
Fix for new Isabelle (primrec)
|
changeset |
files
|
Thu, 18 Feb 2010 11:19:16 +0100 |
Cezary Kaliszyk |
Automatic lifting of constants.
|
changeset |
files
|
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
|