Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <09968-0@swan.cl.cam.ac.uk>; Fri, 1 May 1992 14:01:32 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17287;
          Fri, 1 May 92 05:52:33 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA17283;
          Fri, 1 May 92 05:52:24 -0700
Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk 
          with SMTP (PP-6.0) to cl id <09705-0@swan.cl.cam.ac.uk>;
          Fri, 1 May 1992 13:51:11 +0100
To: hall@edu.uidaho.cs.cheetah
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: Problems with inject_input and ML_eval in 2.0b?
In-Reply-To: Your message of Wed, 29 Apr 92 13:15:02 -0700. <199204292015.AA22888@cheetah.cs.uidaho.edu>
Date: Fri, 01 May 92 13:50:59 +0100
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.722:01.04.92.12.51.27"@cl.cam.ac.uk>


> I'm having some problems getting inject_input and ML_eval to work.
> Maybe someone out there can help me?

ML_eval, at least, has always been rather flaky.  It is, moreover,
not something you're likely to find in HOL90.  I would suggest not
to use it.

Tom