| Mon, 28 Feb 2011 15:21:10 +0000 |
Christian Urban |
split the library into a basics file; merged Nominal_Eqvt into Nominal_Base
|
file |
diff |
annotate
|
| Wed, 16 Feb 2011 14:44:33 +0000 |
Christian Urban |
added eqvt for length
|
file |
diff |
annotate
|
| Wed, 16 Feb 2011 14:03:26 +0000 |
Christian Urban |
added eqvt lemmas for filter and distinct
|
file |
diff |
annotate
|
| Mon, 07 Feb 2011 16:00:24 +0000 |
Christian Urban |
added eqvt for cartesian products
|
file |
diff |
annotate
|
| Wed, 19 Jan 2011 18:07:29 +0100 |
Christian Urban |
added eqvt and supp lemma for removeAll (function from List.thy)
|
file |
diff |
annotate
|
| Tue, 18 Jan 2011 21:26:58 +0100 |
Christian Urban |
some tryes about substitution over type-schemes
|
file |
diff |
annotate
|
| Tue, 18 Jan 2011 17:19:50 +0100 |
Christian Urban |
removed finiteness assumption from set_rename_perm
|
file |
diff |
annotate
|
| Tue, 18 Jan 2011 06:55:18 +0100 |
Christian Urban |
modified the renaming_perm lemmas
|
file |
diff |
annotate
|
| Mon, 17 Jan 2011 17:20:21 +0100 |
Christian Urban |
added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
|
file |
diff |
annotate
|
| Mon, 17 Jan 2011 12:34:11 +0000 |
Christian Urban |
moved high level code from LamTest into the main libraries.
|
file |
diff |
annotate
|
| Thu, 13 Jan 2011 12:12:47 +0000 |
Christian Urban |
added eqvt_lemmas for subset and psubset
|
file |
diff |
annotate
|
| Fri, 07 Jan 2011 05:06:25 +0000 |
Christian Urban |
equivariance of THE_default under the uniqueness assumption
|
file |
diff |
annotate
|
| Thu, 06 Jan 2011 13:28:19 +0000 |
Christian Urban |
same
|
file |
diff |
annotate
|
| Mon, 03 Jan 2011 16:19:27 +0000 |
Christian Urban |
simple cases for string rule inductions
|
file |
diff |
annotate
|