| changeset 2292 | d134bd4f6d1b |
| parent 2288 | 3b83960f9544 |
| child 2293 | aecebd5ed424 |
| 2291:20ee31bc34d5 | 2292:d134bd4f6d1b |
|---|---|
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 ML {* print_depth 50 *} |
7 ML {* print_depth 50 *} |
8 declare [[STEPS = 19]] |
8 declare [[STEPS = 4]] |
9 |
9 |
10 nominal_datatype trm = |
10 nominal_datatype trm = |
11 Var "name" |
11 Var "name" |
12 | App "trm" "trm" |
12 | App "trm" "trm" |
13 | Lam x::"name" t::"trm" bind_set x in t |
13 | Lam x::"name" t::"trm" bind_set x in t |