| changeset 1608 | 304bd7400a47 |
| parent 1604 | 5ab97f43ec24 |
| child 1656 | c9d3dda79fe3 |
| 1607:ac69ed8303cc | 1608:304bd7400a47 |
|---|---|
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 |