equal
deleted
inserted
replaced
1 theory Modules |
1 theory Modules |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
5 (* example from Leroy'96 about modules; |
5 (* |
6 see OTT example by Owens *) |
6 example from Leroy'96 about modules |
|
7 |
|
8 see OTT example by Owens |
|
9 *) |
7 |
10 |
8 atom_decl name |
11 atom_decl name |
9 |
|
10 declare [[STEPS = 31]] |
|
11 |
|
12 |
12 |
13 nominal_datatype modules: |
13 nominal_datatype modules: |
14 mexp = |
14 mexp = |
15 Acc "path" |
15 Acc "path" |
16 | Stru "body" |
16 | Stru "body" |
70 thm modules.bn_defs |
70 thm modules.bn_defs |
71 thm modules.perm_simps |
71 thm modules.perm_simps |
72 thm modules.eq_iff |
72 thm modules.eq_iff |
73 thm modules.fv_bn_eqvt |
73 thm modules.fv_bn_eqvt |
74 thm modules.size_eqvt |
74 thm modules.size_eqvt |
75 |
75 thm modules.supp |
76 |
76 |
77 |
77 |
78 end |
78 end |
79 |
79 |
80 |
80 |