equal
deleted
inserted
replaced
4 |
4 |
5 text {* example 3 or example 5 from Terms.thy *} |
5 text {* example 3 or example 5 from Terms.thy *} |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 ML {* val _ = recursive := false *} |
9 ML {* val _ = recursive := true *} |
10 ML {* val _ = alpha_type := AlphaLst *} |
10 ML {* val _ = alpha_type := AlphaLst *} |
11 nominal_datatype trm = |
11 nominal_datatype trm = |
12 Vr "name" |
12 Vr "name" |
13 | Ap "trm" "trm" |
13 | Ap "trm" "trm" |
14 | Lm x::"name" t::"trm" bind x in t |
14 | Lm x::"name" t::"trm" bind x in t |
34 thm trm_lts.inducts[no_vars] |
34 thm trm_lts.inducts[no_vars] |
35 thm trm_lts.distinct |
35 thm trm_lts.distinct |
36 (*thm trm_lts.supp*) |
36 (*thm trm_lts.supp*) |
37 thm trm_lts.fv[simplified trm_lts.supp(1-2)] |
37 thm trm_lts.fv[simplified trm_lts.supp(1-2)] |
38 |
38 |
|
39 |
39 primrec |
40 primrec |
40 permute_bn_raw |
41 permute_bn_raw |
41 where |
42 where |
42 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |
43 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |
43 | "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \<bullet> a) t (permute_bn_raw pi l)" |
44 | "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \<bullet> a) t (permute_bn_raw pi l)" |