equal
deleted
inserted
replaced
48 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
48 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
49 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
49 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
50 | "b_fnclause (K x pat exp) = {atom x}" |
50 | "b_fnclause (K x pat exp) = {atom x}" |
51 |
51 |
52 |
52 |
53 |
53 thm fun_recs.permute_bn |
54 thm fun_recs.perm_bn_alpha |
54 thm fun_recs.perm_bn_alpha |
55 thm fun_recs.perm_bn_simps |
55 thm fun_recs.perm_bn_simps |
56 thm fun_recs.bn_finite |
56 thm fun_recs.bn_finite |
57 thm fun_recs.inducts |
57 thm fun_recs.inducts |
58 thm fun_recs.distinct |
58 thm fun_recs.distinct |