| Fri, 30 Apr 2010 15:36:02 +0100 |
Christian Urban |
generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements)
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 08:32:33 +0200 |
Christian Urban |
use the more general type-class at_base
|
file |
diff |
annotate
|
| Thu, 22 Apr 2010 05:16:23 +0200 |
Christian Urban |
moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms
|
file |
diff |
annotate
|
| Tue, 13 Apr 2010 07:40:54 +0200 |
Christian Urban |
made everything to compile
|
file |
diff |
annotate
|
| Tue, 13 Apr 2010 00:47:57 +0200 |
Christian Urban |
moved equivariance of map into Nominal2_Eqvt file
|
file |
diff |
annotate
|
| Sun, 11 Apr 2010 18:11:23 +0200 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
| Thu, 08 Apr 2010 00:00:21 -0700 |
Brian Huffman |
simplify instance proof
|
file |
diff |
annotate
|
| Sun, 04 Apr 2010 21:39:28 +0200 |
Christian Urban |
separated general nominal theory into separate folder
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 14:38:22 +0100 |
Cezary Kaliszyk |
Remove list_eq notation.
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 09:21:43 +0100 |
Cezary Kaliszyk |
Generalize Abs_eq_iff.
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 10:15:46 +0100 |
Cezary Kaliszyk |
Strong induction for Type Schemes.
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 12:22:10 +0100 |
Cezary Kaliszyk |
Showed the instance: fset::(at) fs
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 08:31:43 +0100 |
Cezary Kaliszyk |
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
|
file |
diff |
annotate
|