Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 9 Aug 1995 22:17:11 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA160561456; Wed, 9 Aug 1995 14:50:56 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from simon.cs.cornell.edu by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA160531454; Wed, 9 Aug 1995 14:50:54 -0600 Received: from cloyd.cs.cornell.edu (CLOYD.CS.CORNELL.EDU [128.84.227.15]) by simon.cs.cornell.edu (8.6.10/R1.01) with ESMTP id QAA16190 for ; Wed, 9 Aug 1995 16:51:07 -0400 Received: from rocky.cs.cornell.edu (ROCKY.CS.CORNELL.EDU [128.84.254.183]) by cloyd.cs.cornell.edu (8.6.10/M1.6) with ESMTP id QAA13784; Wed, 9 Aug 1995 16:50:55 -0400 From: Miriam Leeser Received: (mel@localhost) by rocky.cs.cornell.edu (8.6.10/C1.3) id QAA26139; Wed, 9 Aug 1995 16:50:53 -0400 Date: Wed, 9 Aug 1995 16:50:53 -0400 Message-Id: <199508092050.QAA26139@rocky.cs.cornell.edu> To: info-hol@leopard.cs.byu.edu Subject: has anyone done chapter 6 of the tutuorial in hol90 I am working through the HOL tutorial in HOL90. I got as far as section 6.4, where you define the function "lines" (page 59 of my tutorial). Does someone have an SML version of the lines function ? Is there a better way to do this ? Note my new email address: Miriam.Leeser@cornell.edu Thanks, Miriam