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; Thu, 28 Jul 1994 11:49:56 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA28423;
          Thu, 28 Jul 1994 04:41:47 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA28419;
          Thu, 28 Jul 1994 04:41:44 -0600
Received: from hawaii.dcs.gla.ac.uk by goggins.dcs.gla.ac.uk 
          with LOCAL SMTP (PP) id <22431-0@goggins.dcs.gla.ac.uk>;
          Thu, 28 Jul 1994 11:36:49 +0100
Received: by hawaii.dcs.gla.ac.uk (4.1/Dumb) id AA25774;
          Thu, 28 Jul 94 11:36:45 BST
From: tfm <tfm@dcs.gla.ac.uk>
Message-Id: <9407281036.AA25774@hawaii.dcs.gla.ac.uk>
To: reetz <reetz@ira.uka.de>
Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk, 
    slind@informatik.tu-muenchen.de
Subject: Re: problems with prove_induction_thm in hol90.6
In-Reply-To: Your message of "Thu, 28 Jul 94 11:44:03 EDT." <"i80fs2.ira.946:28.06.94.09.44.10"@ira.uka.de>
Date: Thu, 28 Jul 94 11:36:45 +0100


> Using hol90.6, I ran into the following error during
> some type definition:

Well, the error doesn't occur when I try the example in the 
latest development version of hol90.  Here, we get a slightly
different test_thm (note the priming):

 val test_thm =
  |- !f0 f1.
       ?!fn.
         (!x. fn (test1 x) = f0 x) /\ (!t f'. fn (test2 t f') = f1 (fn t) f' t)
  : thm

The induction theorem then runs through fine.  What's puzzling to me 
is the f-prime, which is unnecessary.  Perhaps Konrad knows...

Tom