equal
deleted
inserted
replaced
21 sorry |
21 sorry |
22 |
22 |
23 print_quotients |
23 print_quotients |
24 |
24 |
25 local_setup {* |
25 local_setup {* |
26 make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> |
26 old_make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> |
27 make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> |
27 old_make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> |
28 make_const_def @{binding Lam} @{term "rLam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd |
28 old_make_const_def @{binding Lam} @{term "rLam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd |
29 *} |
29 *} |
|
30 |
|
31 thm Var_def |
|
32 thm App_def |
|
33 thm Lam_def |
30 |
34 |
31 lemma real_alpha: |
35 lemma real_alpha: |
32 assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>s" |
36 assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>s" |
33 shows "Lam a t = Lam b s" |
37 shows "Lam a t = Lam b s" |
34 sorry |
38 sorry |