equal
deleted
inserted
replaced
1 (* Title: Admin/Benchmarks/HOL-datatype/SML.thy |
1 (* Title: Admin/Benchmarks/HOL-datatype/SML.thy |
2 ID: $Id$ |
2 |
|
3 Example from Myra: part of the syntax of SML. |
3 *) |
4 *) |
4 |
5 |
5 theory SML imports Main begin |
6 theory SML imports Main begin |
6 |
|
7 (* ------------------------------------------------------------------------- *) |
|
8 (* Example from Myra: part of the syntax of SML. *) |
|
9 (* ------------------------------------------------------------------------- *) |
|
10 |
7 |
11 datatype |
8 datatype |
12 string = EMPTY_STRING | CONS_STRING nat string |
9 string = EMPTY_STRING | CONS_STRING nat string |
13 |
10 |
14 datatype |
11 datatype |