equal
deleted
inserted
replaced
1 theory Classical |
1 theory Classical |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
5 (* example from my Urban's PhD *) |
5 (* example from Urban's PhD *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 atom_decl coname |
8 atom_decl coname |
9 |
9 |
10 nominal_datatype trm = |
10 nominal_datatype trm = |
17 | ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t |
17 | ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t |
18 |
18 |
19 thm trm.distinct |
19 thm trm.distinct |
20 thm trm.induct |
20 thm trm.induct |
21 thm trm.exhaust |
21 thm trm.exhaust |
|
22 thm trm.strong_exhaust |
|
23 thm trm.strong_exhaust[simplified] |
22 thm trm.fv_defs |
24 thm trm.fv_defs |
23 thm trm.bn_defs |
25 thm trm.bn_defs |
24 thm trm.perm_simps |
26 thm trm.perm_simps |
25 thm trm.eq_iff |
27 thm trm.eq_iff |
26 thm trm.fv_bn_eqvt |
28 thm trm.fv_bn_eqvt |
27 thm trm.size_eqvt |
29 thm trm.size_eqvt |
|
30 thm trm.supp |
|
31 thm trm.supp[simplified] |
28 |
32 |
29 |
33 |
30 |
34 |
31 |
35 |
32 end |
36 end |