Fri, 12 Feb 2010 16:04:10 +0100 |
Cezary Kaliszyk |
renamed 'as' to 'is' everywhere.
|
file |
diff |
annotate
|
Thu, 11 Feb 2010 14:00:00 +0100 |
Cezary Kaliszyk |
Notation available locally
|
file |
diff |
annotate
|
Thu, 11 Feb 2010 10:06:02 +0100 |
Cezary Kaliszyk |
Main renaming + fixes for new Isabelle in IntEx2.
|
file |
diff |
annotate
|
Mon, 08 Feb 2010 13:12:55 +0100 |
Christian Urban |
moved some lemmas to Nominal; updated all files
|
file |
diff |
annotate
|
Tue, 02 Feb 2010 14:55:07 +0100 |
Cezary Kaliszyk |
First experiments in Terms.
|
file |
diff |
annotate
|
Tue, 02 Feb 2010 12:48:12 +0100 |
Cezary Kaliszyk |
Disambiguating the syntax.
|
file |
diff |
annotate
|
Tue, 02 Feb 2010 12:36:01 +0100 |
Cezary Kaliszyk |
Minor uncommited changes from LamEx2.
|
file |
diff |
annotate
|
Tue, 02 Feb 2010 11:56:37 +0100 |
Cezary Kaliszyk |
Some equivariance machinery that comes useful in LF.
|
file |
diff |
annotate
|
Tue, 02 Feb 2010 11:23:17 +0100 |
Cezary Kaliszyk |
Generalized the eqvt proof for single binders.
|
file |
diff |
annotate
|
Tue, 02 Feb 2010 10:20:54 +0100 |
Cezary Kaliszyk |
General alpha_gen_trans for one-variable abstraction.
|
file |
diff |
annotate
|
Tue, 02 Feb 2010 09:51:39 +0100 |
Cezary Kaliszyk |
With unfolding Rep/Abs_eqvt no longer needed.
|
file |
diff |
annotate
|
Tue, 02 Feb 2010 08:16:34 +0100 |
Cezary Kaliszyk |
Lam2 finished apart from Rep_eqvt.
|
file |
diff |
annotate
|
Mon, 01 Feb 2010 16:05:59 +0100 |
Cezary Kaliszyk |
All should be ok now.
|
file |
diff |
annotate
|
Mon, 01 Feb 2010 15:57:37 +0100 |
Cezary Kaliszyk |
Fixed wrong rename.
|
file |
diff |
annotate
|