| changeset 766 | df053507edba |
| parent 758 | 3104d62e7a16 |
| child 767 | 37285ec4387d |
| 765:d0250d01782c | 766:df053507edba |
|---|---|
48 |
48 |
49 lemma alpha_equivp: |
49 lemma alpha_equivp: |
50 shows "equivp alpha" |
50 shows "equivp alpha" |
51 sorry |
51 sorry |
52 |
52 |
53 quotient lam = rlam / alpha |
53 quotient_type lam = rlam / alpha |
54 apply(rule alpha_equivp) |
54 apply(rule alpha_equivp) |
55 done |
55 done |
56 |
56 |
57 print_quotients |
57 print_quotients |
58 |
58 |