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