Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <15906-0@swan.cl.cam.ac.uk>; Mon, 17 Aug 1992 17:07:41 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA09105; Mon, 17 Aug 92 08:56:08 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from leopard.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) id AA09100; Mon, 17 Aug 92 08:55:58 -0700 Received: by leopard.cs.uidaho.edu (16.7/1.34) id AA18221; Mon, 17 Aug 92 08:57:34 -0700 From: weiss@edu.uidaho.cs.leopard (Phil Weiss) Message-Id: <9208171557.AA18221@leopard.cs.uidaho.edu> Subject: Function rewrites To: info-hol@edu.uidaho.cs.ted (HOL Mailing List) Date: Mon, 17 Aug 92 8:57:33 PDT Mailer: Elm [revision: 66.33] Another problem: HOL converts definitions of the form foo = (\x. bar) to foo x = bar I was wondering if anyone had written a conversion to rewrite terms of the second form back into the first form. ??? Phil. -- Philip Weiss Laboratory for Applied Logic weiss@leopard.cs.uidaho.edu (Disclaimer: My views are not their views) weiss872@snake.cs.uidaho.edu