| 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
|
| Mon, 29 Nov 2010 08:01:09 +0000 |
Christian Urban |
isarfied some of the high-level proofs
|
file |
diff |
annotate
|
| Sun, 14 Nov 2010 16:34:47 +0000 |
Christian Urban |
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
|
file |
diff |
annotate
| base
|
| Thu, 11 Mar 2010 15:10:07 +0100 |
Christian Urban |
finally the proof that new and old alpha agree
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 14:22:58 +0100 |
Cezary Kaliszyk |
Fix eqvt for multiple quantifiers.
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 11:42:15 +0100 |
Cezary Kaliszyk |
weird eqvt
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 17:11:58 +0100 |
Cezary Kaliszyk |
Add image_eqvt and atom_eqvt to eqvt bases.
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 07:48:33 +0100 |
Christian Urban |
moved Nominal to "toplevel"
|
file |
diff |
annotate
| base
|