| changeset 58329 | a31404ec7414 |
| child 58889 | 5b7a9633cfa8 |
| 58328:086193f231ea | 58329:a31404ec7414 |
|---|---|
1 (* Author: Christian Urban TU Muenchen *) |
|
2 |
|
3 header {* Various examples involving nominal datatypes. *} |
|
4 |
|
5 theory Nominal_Examples_Base |
|
6 imports |
|
7 CK_Machine |
|
8 CR |
|
9 CR_Takahashi |
|
10 Compile |
|
11 Contexts |
|
12 Crary |
|
13 Fsub |
|
14 Height |
|
15 Lambda_mu |
|
16 LocalWeakening |
|
17 Pattern |
|
18 SN |
|
19 SOS |
|
20 Standardization |
|
21 Support |
|
22 Type_Preservation |
|
23 W |
|
24 Weakening |
|
25 begin |
|
26 |
|
27 end |