changeset 16417 | 9bc16273c2d4 |
parent 7373 | 776d888472aa |
child 33695 | bec342db1bf4 |
--- a/Admin/Benchmarks/HOL-datatype/SML.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/Admin/Benchmarks/HOL-datatype/SML.thy Fri Jun 17 16:12:49 2005 +0200 @@ -2,7 +2,7 @@ ID: $Id$ *) -theory SML = Main: +theory SML imports Main begin (* ------------------------------------------------------------------------- *) (* Example from Myra: part of the syntax of SML. *)