Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Fri, 16 Apr 1993 10:09:14 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05130;
          Fri, 16 Apr 93 01:59:28 -0700
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 AA05125;
          Fri, 16 Apr 93 01:59:19 -0700
Received: from heron.cl.cam.ac.uk (user ww (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Fri, 16 Apr 1993 09:57:02 +0100
To: info-hol@edu.uidaho.cs.ted
Subject: A new library res_quan
Date: Fri, 16 Apr 93 09:56:44 +0100
From: Wai Wong <Wai.Wong@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.399:16.04.93.08.57.05"@cl.cam.ac.uk>


A new HOL library res_quan has been added to HOL88 Version 2.02.
The purpose of this library is for handling restricted
quantifications. The library contains a theory which has a small
number of theorems about restricted quantifiers and a set of
ML functions which can be divided into the follow groups:
	syntax function,
	derived rule,
	conversions,
	tactics,
	constant definition functions, and
	conditional rewriting tools.
The last group can be loaded  as a library part without loading
other functions. A complete manual is included.

Before HOL88 Version 2.02 is released, this library is available by
anonymous ftp from ftp.cl.cam.ac.uk in the directory contrib. It
also works in HOL version 2.01.

Wai