author | wenzelm |
Sun, 02 Nov 2014 18:21:45 +0100 | |
changeset 58889 | 5b7a9633cfa8 |
parent 58329 | a31404ec7414 |
permissions | -rw-r--r-- |
58329 | 1 |
(* Author: Christian Urban TU Muenchen *) |
2 |
||
58889 | 3 |
section {* Various examples involving nominal datatypes. *} |
58329 | 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 |