Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <07318-0@swan.cl.cam.ac.uk>; Fri, 24 Jul 1992 10:05:20 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11453; Fri, 24 Jul 92 01:55:26 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA11448; Fri, 24 Jul 92 01:55:19 -0700 Received: from cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <07018-0@swan.cl.cam.ac.uk>; Fri, 24 Jul 1992 09:56:11 +0100 To: info-hol@edu.uidaho.cs.ted Subject: Restricted quantifiers Date: Fri, 24 Jul 92 09:55:53 +0100 From: Wai Wong Message-Id: <"swan.cl.ca.032:24.06.92.08.56.24"@cl.cam.ac.uk> I've been using restricted quantifiers for a while. I now got a small collection of rules, conversions and tactics for dealing with these quantifiers. I'd like to make up a library supporting these. Anyone who has used restricted quantifiers are more than welcome to send me their codes for supporting these quantifiers. I'll do my best to create a general library of restricted quantifiers. --------------------------------- Wai Wong ww@cl.cam.ac.uk University of Cambridge Computer laboratory Cambridge CB2 3QG Tel:+44 223 334688 England =========================================================================