Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 4 Oct 1993 02:45:50 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA17870;
          Sun, 3 Oct 93 18:34:33 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from coffee.cs.uidaho.edu by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA17866; Sun, 3 Oct 93 18:34:31 -0700
Received: by coffee.cs.uidaho.edu (1.37.109.4/16.2) id AA11002;
          Sun, 3 Oct 93 18:28:21 -0700
Date: Sun, 3 Oct 93 18:28:21 -0700
From: toshok@cs.uidaho.edu
To: info-hol@cs.uidaho.edu
Subject: Problem with HOL90 abs-theory package.
Message-ID: <"swan.cl.cam.:018190:931004014629"@cl.cam.ac.uk>

Hello all,

  In trying to get everything going here with hol90, I have tried to use
the abstract theory package ported to hol90 by David Shepherd, and written
by Phil Windley.  I have, however, run into problems.  I tried the examples
given in the documentation that accompanied the package with hol90 (the
monoid example), and it didn't work.  I retyped it several times (thinking I
had simply made a typing error), but it failed to work.  Is there anyone who
has successfully used this package in hol90?  I am using hol90.6, if that
makes any difference.

Thanks for any and all information.

Chris Toshok
Laboratory for Applied Logic
University of Idaho
cs.uidaho.edu