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