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 declare alpha_gen_eqvt[eqvt] |
|
54 |
|
55 equivariance alpha_exp_raw |
51 end |
56 end |
52 |
57 |
53 |
58 |
54 |
59 |