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; Thu, 1 Dec 1994 18:23:51 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA11755;
          Thu, 1 Dec 1994 11:06:59 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from jaguar.cs.byu.edu by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA11751;
          Thu, 1 Dec 1994 11:06:58 -0700
Received: from localhost by jaguar.cs.byu.edu (1.38.193.4/CS-Client) id AA27889;
          Thu, 1 Dec 1994 11:07:06 -0700
Message-Id: <9412011807.AA27889@jaguar.cs.byu.edu>
To: info-hol@leopard.cs.byu.edu
Subject: extracting common terms in HOL
Date: Thu, 01 Dec 1994 11:07:05 -0700
From: Phil Windley <windley@lal.cs.byu.edu>


Hi All,

let_CONV will reduce let expressions in HOL terms.

Has anyone ever done the opposite: taken a large HOL term and extracted
common terms into lets?  

--phil--