equal
deleted
inserted
replaced
5 (* example from my Urban's PhD *) |
5 (* example from my Urban's PhD *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 atom_decl coname |
8 atom_decl coname |
9 |
9 |
10 declare [[STEPS = 9]] |
10 declare [[STEPS = 21]] |
11 |
11 |
12 nominal_datatype trm = |
12 nominal_datatype trm = |
13 Ax "name" "coname" |
13 Ax "name" "coname" |
14 | Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 |
14 | Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 |
15 | AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2 |
15 | AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2 |
16 | AndL1 n::"name" t::"trm" "name" bind n in t |
16 | AndL1 n::"name" t::"trm" "name" bind n in t |
17 | AndL2 n::"name" t::"trm" "name" bind n in t |
17 | AndL2 n::"name" t::"trm" "name" bind n in t |
18 | ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 |
18 | ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 |
19 | ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t |
19 | ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t |
20 |
20 |
21 thm alpha_trm_raw.intros[no_vars] |
21 thm distinct |
|
22 thm induct |
|
23 thm exhaust |
|
24 thm fv_defs |
|
25 thm bn_defs |
|
26 thm perm_simps |
|
27 thm eq_iff |
|
28 thm fv_bn_eqvt |
|
29 thm size_eqvt |
22 |
30 |
23 (* |
31 |
24 thm trm.fv |
|
25 thm trm.eq_iff |
|
26 thm trm.bn |
|
27 thm trm.perm |
|
28 thm trm.induct |
|
29 thm trm.distinct |
|
30 thm trm.fv[simplified trm.supp] |
|
31 *) |
|
32 |
32 |
33 |
33 |
34 end |
34 end |
35 |
35 |
36 |
36 |