Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 21 Dec 1993 22:21:00 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA02733;
          Tue, 21 Dec 1993 15:04:40 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA02729;
          Tue, 21 Dec 1993 15:04:38 -0700
Received: from Maui.CS.UCLA.EDU by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA17256;
          Tue, 21 Dec 1993 14:02:39 -0800
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.23) id AA07443;
          Tue, 21 Dec 93 14:02:37 -0800
Message-Id: <9312212202.AA07443@maui.cs.ucla.edu>
To: info-hol@cs.uidaho.edu
Subject: HOL vs Church's Simple Type Theory
Date: Tue, 21 Dec 93 14:02:36 PST
From: chou@cs.ucla.edu

What are the extensions that HOL made with respect to 

the original Simple Type Theory of Church?  There are
two that I know of:

(1) Object-level type variables.

(2) Constant and type definitions.

Anything else?

Thanks in advance!

- Ching Tsun