equal
deleted
inserted
replaced
1 theory ExLetMult |
1 theory ExLetMult |
2 imports "../Parser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 ML {* val _ = recursive := true *} |
|
8 ML {* val _ = alpha_type := AlphaLst *} |
|
9 ML {* val _ = cheat_equivp := true *} |
|
10 nominal_datatype trm = |
7 nominal_datatype trm = |
11 Vr "name" |
8 Vr "name" |
12 | Ap "trm" "trm" |
9 | Ap "trm" "trm" |
13 | Lm x::"name" t::"trm" bind x in t |
10 | Lm x::"name" t::"trm" bind_set x in t |
14 | Lt l::"lts" t::"trm" s::"trm" bind "bn l" in t, bind "bn l" in s |
11 | Lt l::"lts" t::"trm" s::"trm" bind "bn l" in t s |
15 and lts = |
12 and lts = |
16 Lnil |
13 Lnil |
17 | Lcons "name" "trm" "lts" |
14 | Lcons "name" "trm" "lts" |
18 binder |
15 binder |
19 bn |
16 bn |