equal
deleted
inserted
replaced
46 | "b_fnclause (K x pat exp) = {atom x}" |
46 | "b_fnclause (K x pat exp) = {atom x}" |
47 |
47 |
48 thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv |
48 thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv |
49 thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff |
49 thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff |
50 |
50 |
51 |
|
52 declare permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[eqvt] |
|
53 |
|
54 equivariance alpha_exp_raw |
51 equivariance alpha_exp_raw |
55 end |
52 end |
56 |
53 |
57 |
54 |
58 |
55 |