Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
From: shaw@cs.ucdavis.edu (Rob Shaw)
Date: Mon, 9 Oct 1995 16:54:52 -0700
Message-Id: <199510092354.QAA19306@roma-cafe.cs.ucdavis.edu>
To: info-hol@cs.uidaho.edu
Subject: ACCEPT_TAC nit pick...
Content-Length: 643


Hi, why does HOL90 behave in the following way? (not giving you your actual
goal term as the resulting theorem, but rather the thm you gave to ACCEPT_TAC)

- val th1 = theorem "prim_rec" "LESS_REFL";
val th1 = |- !n. ~(n < n) : thm
- g `!m. ~(m < m)`;
val it =
  Status: 1 proof.
  1. Incomplete:
       Initial goal:
       (--`!m. ~(m < m)`--)
       
       
   : proofs
- e( ACCEPT_TAC th1 );
OK..
val it =
  Initial goal proved.
  |- !n. ~(n < n) : goalstack
- top_thm();
val it = |- !n. ~(n < n) : thm

It seems to me that for consistency shouldn't you always get a thm whose 
conclusion is exactly the goal term you want?

Thanx!

Rob