changeset 272 | ddd2f209d0d2 |
parent 271 | 1b57f99737fe |
child 273 | b82e765ca464 |
271:1b57f99737fe | 272:ddd2f209d0d2 |
---|---|
32 |
32 |
33 print_theorems |
33 print_theorems |
34 |
34 |
35 lemma alpha_refl: |
35 lemma alpha_refl: |
36 shows "x \<approx> x" |
36 shows "x \<approx> x" |
37 apply (rule rlam.induct) |
|
38 apply (simp_all add:a1 a2) |
|
39 apply (rule a3) |
|
40 apply (simp_all) |
|
37 sorry |
41 sorry |
38 |
42 |
39 quotient lam = rlam / alpha |
43 quotient lam = rlam / alpha |
40 sorry |
44 sorry |
41 |
45 |