Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Wed, 31 Mar 1993 15:48:59 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07243; Wed, 31 Mar 93 06:30:47 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA07238; Wed, 31 Mar 93 06:30:36 -0800 Received: from heron.cl.cam.ac.uk (user ww (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Wed, 31 Mar 1993 15:29:17 +0100 To: Wishnu Prasetya Cc: info-hol@edu.uidaho.cs.ted (hol mailing list), Wai.Wong@uk.ac.cam.cl Subject: Re: Restricted Quantifier problem In-Reply-To: Your message of Wed, 31 Mar 93 15:49:16 +0100. <199303311349.AA14410@infix.cs.ruu.nl> Date: Wed, 31 Mar 93 15:29:02 +0100 From: Wai Wong Message-Id: <"swan.cl.ca.871:31.03.93.14.29.25"@cl.cam.ac.uk> Hi, I've just tried a simple example as you desribed in your message. It works. Here is the transcript of the session: *albatross> hol =============================================================================== HOL88 Version 2.01 (SUN4/AKCL), built on 4/12/92 =============================================================================== #new_theory`foo`;; () : void #let FOO = new_binder_definition(`FOO`,"$!! = $!:(*->bool)->bool");; FOO = |- $!! = $! #let RES_FOO = new_definition(`RES_FOO`, "RES_FOO P B = !x:*. P x ==> B x");; RES_FOO = |- !P B. RES_FOO P B = (!x. P x ==> B x) #associate_restriction(`!!`, `RES_FOO`);; () : void #"!!x:*::P.B";; "!! x :: P. B" : term #close_theory();; () : void #quit();; Bye. *albatross> hol =============================================================================== HOL88 Version 2.01 (SUN4/AKCL), built on 4/12/92 =============================================================================== #new_theory`baa`;; () : void #new_parent`foo`;; Theory foo loaded () : void #"!!x:*::P.B";; no restriction constant associated with !! skipping: B " ;; parse failed #associate_restriction(`!!`, `RES_FOO`);; () : void #"!!x:*::P.B";; "!! x :: P. B" : term Wai