Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <12482-0@swan.cl.cam.ac.uk>; Sat, 18 Jul 1992 01:14:19 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17274; Fri, 17 Jul 92 17:03:49 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from leopard.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) id AA17269; Fri, 17 Jul 92 17:03:44 -0700 Received: by leopard.cs.uidaho.edu (16.7/1.34) id AA00661; Fri, 17 Jul 92 17:06:52 -0700 From: weiss@edu.uidaho.cs.leopard (Phil Weiss) Message-Id: <9207180006.AA00661@leopard.cs.uidaho.edu> Subject: Figured it out (set recursion) To: info-hol@edu.uidaho.cs.ted (HOL Mailing List) Date: Fri, 17 Jul 92 17:06:52 PDT Mailer: Elm [revision: 66.33] I had a function: change_foo foo x_set and change_foo_sing foo x change_foo could easily be defined as (\x. (x IN x_set) => (change_foo_sing foo x) x | foo x) I have no clue why I didn't figure this out sooner. Phil. -- Philip Weiss Laboratory for Applied Logic weiss@leopard.cs.uidaho.edu (Disclaimer: My views are not their views) weiss872@snake.cs.uidaho.edu