equal
deleted
inserted
replaced
1 theory Lambda |
1 theory Lambda |
2 imports "../Parser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 nominal_datatype lam = |
7 nominal_datatype lam = |
8 Var "name" |
8 Var "name" |
9 | App "lam" "lam" |
9 | App "lam" "lam" |
10 | Lam x::"name" l::"lam" bind x in l |
10 | Lam x::"name" l::"lam" bind_set x in l |
11 |
11 |
12 thm lam.fv |
12 thm lam.fv |
13 thm lam.supp |
13 thm lam.supp |
14 lemmas supp_fn' = lam.fv[simplified lam.supp] |
14 lemmas supp_fn' = lam.fv[simplified lam.supp] |
15 |
15 |
16 declare lam.perm[eqvt] |
16 declare lam.perm[eqvt] |
17 |
17 |
18 section {* Strong Induction Principles*} |
18 section {* Strong Induction Principles*} |
19 |
19 |
20 (* |
20 (* |
21 Old way of establishing strong induction |
21 Old way of establishing strong induction |
22 principles by chosing a fresh name. |
22 principles by chosing a fresh name. |
23 *) |
23 *) |
24 lemma |
24 lemma |
25 fixes c::"'a::fs" |
25 fixes c::"'a::fs" |