Return-Path: <info-hol-request@lal.cs.byu.edu>
Delivery-Date: 
Received: from bescot.cl.cam.ac.uk (user exim (mailer)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Wed, 13 Dec 1995 17:59:21 +0000
Received: from leopard.cs.byu.edu [128.187.2.182] by bescot.cl.cam.ac.uk 
          with esmtp (Exim 0.24 #26) id E0tPvRo-0000Ys-00;
          Wed, 13 Dec 1995 17:58:43 +0000
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA154445683;
          Wed, 13 Dec 1995 07:41:23 -0700
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 AA154415681;
          Wed, 13 Dec 1995 07:41:21 -0700
Received: from aohakobe (localhost [127.0.0.1]) 
          by aohakobe.ipc.chiba-u.ac.jp (8.6.12/3.4Wbeta3 (-: 95041617) 
          with ESMTP id XAA06644 for <info-hol@leopard.cs.byu.edu>;
          Wed, 13 Dec 1995 23:42:23 +0900
Message-Id: <199512131442.XAA06644@aohakobe.ipc.chiba-u.ac.jp>
To: info-hol@leopard.cs.byu.edu
Subject: Re: Is anybody know how to install HOL via Lucid Lisp ?
In-Reply-To: Your message of "Mon, 11 Dec 1995 18:23:31 EST." <199512112323.SAA14539@dialup.math.ncsu.edu>
Date: Wed, 13 Dec 1995 23:42:23 +0900
From: Yozo Toda (TELEPHONE +81-43-290-3539) <yozo@aohakobe.ipc.chiba-u.ac.jp>


I'm not a real HOL user, but...

> most everything i knew. (Even I did compile ml/ml-curry.) It has been almost 
> 1 month since I tried to install HOL. After knowing LCF, I really want to
> use HOL to know its power. Please, help me. Thank you for your time.

how about trying other Lisp system?  kcl, akcl, gcl...
or you should try HOL90 (on SML-NJ) if you have no reason to stick to HOL88.
Many proof-checking environments (Isabelle, Lego, ELF, ...) are built on SML.

BTW, I found Mr.Paulson put LCF package in his FTP area (-:

-- yozo.