| changeset 2120 | 2786ff1df475 |
| parent 2105 | e25b0fff0dd2 |
| 2119:238062c4c9f2 | 2120:2786ff1df475 |
|---|---|
32 thm trm_lts.inducts[no_vars] |
32 thm trm_lts.inducts[no_vars] |
33 thm trm_lts.distinct |
33 thm trm_lts.distinct |
34 (*thm trm_lts.supp*) |
34 (*thm trm_lts.supp*) |
35 thm trm_lts.fv[simplified trm_lts.supp(1-2)] |
35 thm trm_lts.fv[simplified trm_lts.supp(1-2)] |
36 |
36 |
37 equivariance alpha_bn_raw |
|
38 |
37 |
39 primrec |
38 primrec |
40 permute_bn_raw |
39 permute_bn_raw |
41 where |
40 where |
42 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |
41 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |