equal
deleted
inserted
replaced
26 thm trm_assn.induct |
26 thm trm_assn.induct |
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[where y="t", no_vars] |
32 |
32 |
33 primrec |
33 primrec |
34 permute_bn_raw |
34 permute_bn_raw |
35 where |
35 where |
36 "permute_bn_raw p (ANil_raw) = ANil_raw" |
36 "permute_bn_raw p (ANil_raw) = ANil_raw" |