| changeset 1598 | 2406350c358f |
| parent 1597 | af34dd3418fe |
| 1597:af34dd3418fe | 1598:2406350c358f |
|---|---|
1 theory Ex3 |
1 theory Ex3 |
2 imports "Parser" |
2 imports "Parser" |
3 begin |
3 begin |
4 |
|
5 (* Example 3, identical to example 1 from Terms.thy *) |
|
4 |
6 |
5 atom_decl name |
7 atom_decl name |
6 |
8 |
7 ML {* val _ = recursive := false *} |
9 ML {* val _ = recursive := false *} |
8 nominal_datatype trm0 = |
10 nominal_datatype trm0 = |