Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 24 Nov 1993 10:01:01 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA02122; Wed, 24 Nov 1993 02:54:36 -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 AA02118; Wed, 24 Nov 1993 02:54:33 -0700 Received: from iraun1.ira.uka.de by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA06560; Wed, 24 Nov 93 01:52:17 -0800 Received: from ira.uka.de by iraun1.ira.uka.de id <11466-0@iraun1.ira.uka.de>; Wed, 24 Nov 1993 10:52:03 +0100 Received: from ira.uka.de by irafs2.ira.uka.de id <25984-0@irafs2.ira.uka.de>; Wed, 24 Nov 1993 10:51:59 +0100 Date: Wed, 24 Nov 93 10:51:15 EST From: reetz To: info-hol@cs.uidaho.edu Subject: RE: undefined value Message-Id: <"irafs2.ira.986:24.10.93.09.52.01"@ira.uka.de> maybe you should define a constant undefined_value with the desired property: val th = prove(--` ?undefined_value. undefined_value i l = ~(i in bounds l) `--, ... ); new_specification {name = "undefined_value", sat_thm = th, consts =[{const_name="undefined_value",fixity=Prefix}]}; unfortunately, this constant need i and l as parameter. However, using the property th, this might not be a problem, because it should hold for different i and l. I haven't tested this idea, however. I might be wrong. hope this helps, :) Ralf (*****************************************************************************) (* *) (* Ralf Reetz SFB 358 of the german research society (DFG) *) (* reetz@ira.uka.de University of Karlsruhe, Germany *) (* *) (* "we prove around in a ring and suppose, *) (* the goal sits right in the middle and knows." *) (* *) (*****************************************************************************)