| changeset 1604 | 5ab97f43ec24 |
| parent 1600 | e33e37fd4c7d |
| child 1656 | c9d3dda79fe3 |
| 1603:2b367c80c0d7 | 1604:5ab97f43ec24 |
|---|---|
27 thm exp_pat3.eq_iff |
27 thm exp_pat3.eq_iff |
28 thm exp_pat3.bn |
28 thm exp_pat3.bn |
29 thm exp_pat3.perm |
29 thm exp_pat3.perm |
30 thm exp_pat3.induct |
30 thm exp_pat3.induct |
31 thm exp_pat3.distinct |
31 thm exp_pat3.distinct |
32 thm exp_pat3.fv[simplified exp_pat3.supp] |
32 thm exp_pat3.fv |
33 thm exp_pat3.supp (* The bindings are too complicated *) |
|
33 |
34 |
34 end |
35 end |
35 |
36 |
36 |
37 |
37 |
38 |