LamEx.thy
changeset 272 ddd2f209d0d2
parent 271 1b57f99737fe
child 273 b82e765ca464
equal deleted inserted replaced
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