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; Mon, 31 Oct 1994 17:10:46 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA02918;
          Mon, 31 Oct 1994 10:14:52 -0700
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA02903;
          Mon, 31 Oct 1994 10:14:40 -0700
Received: from woodcock.cl.cam.ac.uk (user mjcg (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Mon, 31 Oct 1994 17:06:00 +0000
Received: by woodcock.cl.cam.ac.uk (4.1/SMI-3.0DEV3) id AA17968;
          Mon, 31 Oct 94 17:05:39 GMT
Date: Mon, 31 Oct 94 17:05:39 GMT
From: Mike.Gordon@cl.cam.ac.uk
Message-Id: <9410311705.AA17968@woodcock.cl.cam.ac.uk>
To: hol2000@leopard.cs.byu.edu
Subject: Two papers on HOL and set theory


The URL:

   http://www.cl.cam.ac.uk/users/mjcg/papers/holst

provides access to the following two new technical reports:

@techreport{Gordon:HOLST94,
  author      = {M.J.C. Gordon},
  title       = {Merging HOL with Set Theory: preliminary experiments},
  institution = {University of Cambridge Computer Laboratory},
  number      = {353},
  year        = 1994}

@techreport{Agerholm:Dinf94,
  author      = {S. Agerholm},
  title       = {Formalising a Model of the $\lambda$-calculus in {HOL-ST}},
  institution = {University of Cambridge Computer Laboratory},
  number      = {354},
  year        = 1994}