| author | Christian Urban <urbanc@in.tum.de> |
| Sun, 14 Nov 2010 11:46:39 +0000 | |
| changeset 2566 | a59d8e1e3a17 |
| parent 2565 | 6bf332360510 |
| permissions | -rw-r--r-- |
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Nominal2_FSet |
|
2467
67b3933c3190
got rid of Nominal_Atoms (folded into Nominal2_Base)
Christian Urban <urbanc@in.tum.de>
parents:
2466
diff
changeset
|
2 |
imports "../Nominal-General/Nominal2_Base" |
|
2565
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents:
2559
diff
changeset
|
3 |
"../Nominal-General/Nominal2_Eqvt" |
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
begin |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
|
|
2004
b96e8cf86891
generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements)
Christian Urban <urbanc@in.tum.de>
parents:
1973
diff
changeset
|
6 |
|
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
|
|
2004
b96e8cf86891
generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements)
Christian Urban <urbanc@in.tum.de>
parents:
1973
diff
changeset
|
8 |
|
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
end |