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; Tue, 2 Aug 1994 08:23:29 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA10596;
          Tue, 2 Aug 1994 01:15:15 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from irafs1.ira.uka.de by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA10592;
          Tue, 2 Aug 1994 01:15:08 -0600
Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP);
          Tue, 2 Aug 1994 09:06:12 +0200
Received: from ira.uka.de by i80fs2.ira.uka.de id <22685-0@i80fs2.ira.uka.de>;
          Tue, 2 Aug 1994 09:13:55 +0200
Date: Tue, 2 Aug 94 9:13:54 EDT
From: reetz <reetz@ira.uka.de>
To: info-hol@leopard.cs.byu.edu
Subject: RE: HOL90 library loading
Message-Id: <"i80fs2.ira.687:02.07.94.07.13.57"@ira.uka.de>

>Why all the warnings and GC's ?
 
Where is nothing unusual with it. GC are part of
SML/NJ 0.93 and have nothing to do with HOL90.6.
To put it frankly, SML/NJ 0.93 is ``well-known''
for its GC in any sense.
 
I'm not familiar with classic ML, so I don't
know whether there's anything new with the
following feature of SML, resulting in the
warnings you have seen:
 
You can define functions partly, e.g.
 
fun foo (_,h::t) =
 ...
 
meaning that foo gets a pair, where
the first argument is skipped by the
wildcard _ and the second argument is
supposed to be a list consisting of
a head h and a tail t (:: is the same
as CONS in the hol logic). So, the functions,
which were loaded as a effect of loading the
library, are sometime only partly defined.
As I said, nothing unusual.
 
hope this helps,
 
Ralf.


(********************************************************)
(*                                                      *)
(*  Ralf Reetz                                          *)
(*                                                      *)
(*  University of Karlsruhe                             *)
(*  Institut fuer Rechnerentwurf und Fehlertoleranz     *)
(*  76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany   *)
(*                                                      *)
(*  e-mail: reetz@ira.uka.de                            *)
(*  WWW:    http://goethe.ira.uka.de/people/reetz.html  *)
(*                                                      *)
(********************************************************)