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
|