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, 23 Nov 1993 05:24:42 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26043;
          Mon, 22 Nov 1993 22:14:11 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA26039;
          Mon, 22 Nov 1993 22:14:10 -0700
Received: from panther.cs.uidaho.edu by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA03543; Mon, 22 Nov 93 21:11:56 -0800
Received: by panther.cs.uidaho.edu id AA20737 (5.65c/IDA-1.4.4 
          for info-hol@cs.uidaho.edu); Mon, 22 Nov 1993 21:10:31 -0800
Date: Mon, 22 Nov 1993 21:10:31 -0800
From: Chris Toshok <toshok@cs.uidaho.edu>
Message-Id: <199311230510.AA20737@panther.cs.uidaho.edu>
To: info-hol@cs.uidaho.edu
Subject: Problem porting

Hello all,

  In the course of trying to port a proof to HOL90 from HOL88, I have run across a 
problem.  In the course of the proof, the following term is generated:

(in hol88):
      "Next(\t'. T)(n,(@t. Next(\t'. T)(n,t))) /\ Next(\t'. T)(n,SUC n)"

(in hol90):
      (--`Next (\t'. T) (n,(@t. Next (\t. T) (n,t))) /\ Next (\t'. T) (n,SUC n)`--)

I use the following command in both versions:

      e (CONV_TAC (DEPTH_CONV SELECT_CONV));;

and hol88 spits out:

      OK..
      "(?t. Next(\t'. T)(n,t)) /\ Next(\t'. T)(n,SUC n)"

while hol90 gives me the same term back:

      - - = = = OK..
      1 subgoal:
      (--`Next (\t'. T) (n,(@t. Next (\t. T) (n,t))) /\ Next (\t'. T) (n,SUC n)`--)


  I don't care that rewriting in hol90 is supposed to be different in some
ways from hol88, but can someone please tell me how to get to the resulting
hol88 term in hol90?

Thanks in advance,
Chris Toshok
toshok@cs.uidaho.edu