| changeset 2120 | 2786ff1df475 |
| parent 2116 | ce228f7b2b72 |
| child 2436 | 3885dc2669f9 |
| 2119:238062c4c9f2 | 2120:2786ff1df475 |
|---|---|
47 | "b_fnclause (K x pat exp) = {atom x}" |
47 | "b_fnclause (K x pat exp) = {atom x}" |
48 |
48 |
49 thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv |
49 thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv |
50 thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff |
50 thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff |
51 |
51 |
52 equivariance alpha_exp_raw |
|
53 end |
52 end |
54 |
53 |
55 |
54 |
56 |
55 |