equal
deleted
inserted
replaced
1 theory Lambda |
1 theory Lambda |
2 imports "../NewParser" Quotient_Option |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 declare [[STEPS = 9]] |
6 declare [[STEPS = 20]] |
7 |
7 |
8 nominal_datatype lam = |
8 nominal_datatype lam = |
9 Var "name" |
9 Var "name" |
10 | App "lam" "lam" |
10 | App "lam" "lam" |
11 | Lam x::"name" l::"lam" bind x in l |
11 | Lam x::"name" l::"lam" bind x in l |
|
12 |
|
13 |
|
14 thm eq_iff |
12 |
15 |
13 thm lam.fv |
16 thm lam.fv |
14 thm lam.supp |
17 thm lam.supp |
15 lemmas supp_fn' = lam.fv[simplified lam.supp] |
18 lemmas supp_fn' = lam.fv[simplified lam.supp] |
16 |
19 |