| changeset 2467 | 67b3933c3190 |
| parent 2466 | 47c840599a6b |
| child 2470 | bdb1eab47161 |
| 2466:47c840599a6b | 2467:67b3933c3190 |
|---|---|
3 |
3 |
4 Supplementary Lemmas and Definitions for |
4 Supplementary Lemmas and Definitions for |
5 Nominal Isabelle. |
5 Nominal Isabelle. |
6 *) |
6 *) |
7 theory Nominal2_Supp |
7 theory Nominal2_Supp |
8 imports Nominal2_Base Nominal2_Eqvt Nominal2_Atoms |
8 imports Nominal2_Base Nominal2_Eqvt |
9 begin |
9 begin |
10 |
10 |
11 |
11 |
12 section {* Fresh-Star *} |
12 section {* Fresh-Star *} |
13 |
13 |