equal
deleted
inserted
replaced
27 thm trm_assn.inducts |
27 thm trm_assn.inducts |
28 thm trm_assn.distinct |
28 thm trm_assn.distinct |
29 thm trm_assn.supp |
29 thm trm_assn.supp |
30 thm trm_assn.fresh |
30 thm trm_assn.fresh |
31 thm trm_assn.exhaust |
31 thm trm_assn.exhaust |
32 |
|
33 |
|
34 lemma fin_bn: |
|
35 shows "finite (set (bn l))" |
|
36 apply(induct l rule: trm_assn.inducts(2)) |
|
37 apply(simp_all) |
|
38 done |
|
39 |
32 |
40 primrec |
33 primrec |
41 permute_bn_raw |
34 permute_bn_raw |
42 where |
35 where |
43 "permute_bn_raw p (ANil_raw) = ANil_raw" |
36 "permute_bn_raw p (ANil_raw) = ANil_raw" |