Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 10 Aug 1995 04:24:58 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA184653362;
          Wed, 9 Aug 1995 20:56:03 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from aohakobe.ipc.chiba-u.ac.jp by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA184623361;
          Wed, 9 Aug 1995 20:56:01 -0600
Received: from aohakobe (localhost [127.0.0.1]) 
          by aohakobe.ipc.chiba-u.ac.jp (8.6.12/3.4Wbeta3 (-: 95041617) 
          with ESMTP id LAA07738; Thu, 10 Aug 1995 11:56:59 +0900
Message-Id: <199508100256.LAA07738@aohakobe.ipc.chiba-u.ac.jp>
To: Miriam.Leeser@cornell.edu
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: has anyone done chapter 6 of the tutuorial in hol90
In-Reply-To: Your message of "Wed, 09 Aug 1995 16:50:53 -0400." <199508092050.QAA26139@rocky.cs.cornell.edu>
Date: Thu, 10 Aug 1995 11:56:59 +0900
From: Yozo Toda (TELEPHONE +81-43-290-3539) <yozo@aohakobe.ipc.chiba-u.ac.jp>


> Does someone have an SML version of the lines function ?

When I tried this tutorial a year ago, I wrote the following:

      fun lines tok t =
        let val x = fst (dest_var(rator(lhs(snd(dest_forall t)))))
        in (mem x (words2 " " tok))
      end;

simply translating to SML.
I didn't think any better way, I'm not a SML guru )-:

-- yozo.