Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <05642-0@swan.cl.cam.ac.uk>; Tue, 16 Jun 1992 12:20:54 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17980; Tue, 16 Jun 92 04:06:14 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from infix.cs.ruu.nl by ted.cs.uidaho.edu (16.6/1.34) id AA17974; Tue, 16 Jun 92 04:06:04 -0700 Received: by infix.cs.ruu.nl id AA16633 (5.65c/IDA-1.4.4 for info-hol@ted.cs.uidaho.edu); Tue, 16 Jun 1992 13:06:38 +0200 From: Wishnu Prasetya Message-Id: <199206161106.AA16633@infix.cs.ruu.nl> Subject: ISPEC definition To: info-hol@edu.uidaho.cs.ted (hol mailing list) Date: Tue, 16 Jun 92 13:06:36 METDST X-Mailer: ELM [version 2.3 PL11] Hi there, I need to define something, which involve built-in rule ISPEC and EXISTENCE. The first instantiates a universal quatification, and if necessary also do type instantiation. The second gives an existence theorem from a unique existence theorem. Both are available in HOL 88 version 2.0,but unfortunately I have an old version (1.11) and upgrading to a newer version is not entirely mine to decide. The definition of EXISTENCE seems quite easy, but I have difficulty with ISPEC. Can someone pass me the definition, or give a direction as to where they would be available? Thank you kindly in advance. -Wishnu Prasetya- CS Dept. Utrecht University, Holland. --