equal
deleted
inserted
replaced
1 theory ExPS7 |
1 theory ExPS7 |
2 imports "../Parser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 (* example 7 from Peter Sewell's bestiary *) |
5 (* example 7 from Peter Sewell's bestiary *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 ML {* val _ = recursive := true *} |
|
10 nominal_datatype exp7 = |
9 nominal_datatype exp7 = |
11 EVar name |
10 EVar name |
12 | EUnit |
11 | EUnit |
13 | EPair exp7 exp7 |
12 | EPair exp7 exp7 |
14 | ELetRec l::"lrbs" e::"exp7" bind "b7s l" in e |
13 | ELetRec l::"lrbs" e::"exp7" bind_set "b7s l" in l e |
15 and lrb = |
14 and lrb = |
16 Assign name exp7 |
15 Assign name exp7 |
17 and lrbs = |
16 and lrbs = |
18 Single lrb |
17 Single lrb |
19 | More lrb lrbs |
18 | More lrb lrbs |