Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0)
          id <28310-0@swan.cl.cam.ac.uk>; Sun, 9 Feb 1992 07:00:20 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06743;
          Sat, 8 Feb 92 22:47:45 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA06739;
          Sat, 8 Feb 92 22:47:40 -0800
Received: from LocalHost.cs.ucla.edu
          by maui.cs.ucla.edu (Sendmail 5.61b+YP/3.13) id AA17805;
          Sat, 8 Feb 92 22:50:06 -0800
Message-Id: <9202090650.AA17805@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Cc: chou@edu.ucla.cs
Subject: Restricted quantification
Date: Sat, 08 Feb 92 22:50:04 PST
From: chou@edu.ucla.cs

Has any of you experienced HOL hackers made serious use of
restricted quantifications (i.e., things like !x::P.F[x])?
I'd like to know how you think about them and what tools
you have written to manipulate them.  Personally I have a
feeling that restricted quantifications can be very useful.
Yet I have so little experience with HOL that I fear my
fondness of them was due entirely to the nice syntax and,
as a practical matter, I really should eschew them.

Your advices will be greatly appreciated.  I will post a
summary if there are enough responses.

- Ching Tsun