Received: from leopard.cs.byu.edu (leopard.cs.byu.edu [128.187.2.182]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id VAA11691; Tue, 10 Oct 1995 21:07:32 +0200 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA265618182; Tue, 10 Oct 1995 12:03:02 -0600 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: list Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA265538179; Tue, 10 Oct 1995 12:02:59 -0600 Received: from vanuata.dcs.gla.ac.uk (vanuata.dcs.gla.ac.uk [130.209.240.50]) by dworshak.cs.uidaho.edu (8.6.12/1.1) with ESMTP id LAA14518 for ; Tue, 10 Oct 1995 11:02:53 -0700 Message-Id: <199510101802.LAA14518@dworshak.cs.uidaho.edu> Received: from gozo.dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk with LOCAL SMTP (PP); Tue, 10 Oct 1995 18:53:52 +0100 To: Konrad Slind Cc: shaw@cs.ucdavis.edu, info-hol@cs.uidaho.edu, tfm@dcs.gla.ac.uk Subject: Re: ACCEPT_TAC nit pick... In-Reply-To: Your message of "Tue, 10 Oct 1995 15:42:41 BST." <95Oct10.154255met.8083@sunbroy14.informatik.tu-muenchen.de> Date: Tue, 10 Oct 1995 18:53:32 +0100 From: Tom Melham > Rob Shaw writes > > > - g `!m. ~(m < m)`; > > ... > > Initial goal proved. > > |- !n. ~(n < n) : goalstack > > This is a place where theory meets practice. Lambda calculus theory (and > HOL) treats alpha-equivalent terms as identical. However, ... > ... Is the > added complexity worth it? I assume Konrad means the added execution time, and not the complexity of the code for ACCEPT_TAC. The point is a very valid one in general. In this case, however, I think that it would be okay to execute the "two tests" -- mu guess is that most of the times ACCEPT_TAC is actually executed is on fairly small terms. Tom