Admin/Benchmarks/HOL-datatype/SML.thy
changeset 16417 9bc16273c2d4
parent 7373 776d888472aa
child 33695 bec342db1bf4
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     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