| changeset 2950 | 0911cb7bf696 |
| parent 2648 | 5d9724ad543d |
| 2949:adf22ee09738 | 2950:0911cb7bf696 |
|---|---|
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" binds x in l |
11 |
11 |
12 thm lam.distinct |
12 thm lam.distinct |
13 thm lam.induct |
13 thm lam.induct |
14 thm lam.exhaust |
14 thm lam.exhaust |
15 thm lam.fv_defs |
15 thm lam.fv_defs |