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; Fri, 18 Nov 1994 17:35:16 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA03046;
          Fri, 18 Nov 1994 10:25:01 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from tuminfo2.informatik.tu-muenchen.de by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA03036;
          Fri, 18 Nov 1994 10:24:37 -0700
Received: by tuminfo2.informatik.tu-muenchen.de via suspension id <26>;
          Fri, 18 Nov 1994 18:20:38 +0100
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) 
          by tuminfo2.informatik.tu-muenchen.de with SMTP id <24>;
          Fri, 18 Nov 1994 18:19:20 +0100
Received: by sunbroy14.informatik.tu-muenchen.de id <8083>;
          Fri, 18 Nov 1994 18:19:12 +0100
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: reetz@ira.uka.de, info-hol@leopard.cs.byu.edu
In-Reply-To: <"i80fs2.ira.484:18.11.94.17.14.11"@ira.uka.de> (message from reetz on Sat, 19 Nov 1994 00:14:06 +0100)
Subject: Re: INL is one-one
Message-Id: <94Nov18.181912met.8083@sunbroy14.informatik.tu-muenchen.de>
Date: Fri, 18 Nov 1994 18:19:00 +0100


> I wonder that INL from theory "sum" is one-one was never proven/
> stored there (same for INR, of course). One might like to add it:

These theorems (INL_11 and INR_11) are proved in the theory "sum", but
not saved. That oversight ought to be remedied. The theorems should also
be added to the underlying base of rewrites.

Konrad.