equal
deleted
inserted
replaced
8 atom_decl name |
8 atom_decl name |
9 |
9 |
10 (* example 4 from Terms.thy *) |
10 (* example 4 from Terms.thy *) |
11 (* fv_eqvt does not work, we need to repaire defined permute functions |
11 (* fv_eqvt does not work, we need to repaire defined permute functions |
12 defined fv and defined alpha... *) |
12 defined fv and defined alpha... *) |
13 (* lists-datastructure does not work yet |
13 (* lists-datastructure does not work yet *) |
14 nominal_datatype trm4 = |
|
15 Vr4 "name" |
|
16 | Ap4 "trm4" "trm4 list" |
|
17 | Lm4 x::"name" t::"trm4" bind x in t |
|
18 |
14 |
|
15 (* |
|
16 nominal_datatype trm = |
|
17 Vr "name" |
|
18 | Ap "trm" "trm list" |
|
19 | Lm x::"name" t::"trm" bind x in t |
|
20 *) |
|
21 |
|
22 (* |
19 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] |
23 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] |
20 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] |
24 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] |
21 *) |
25 *) |
22 |
26 |
23 end |
27 end |