Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Mon, 19 Apr 1993 21:54:15 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13499; Mon, 19 Apr 93 07:09:59 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from BOX.EE.CORNELL.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA13494; Mon, 19 Apr 93 07:09:53 -0700 Received: by box.EE.CORNELL.EDU (4.1/1.6.10+n-y-Cornell-Electrical-Engineering) id AA09397; Mon, 19 Apr 93 10:09:40 EDT Message-Id: <9304191409.AA09397@box.EE.CORNELL.EDU> From: markaa@box.EE.CORNELL.EDU (Mark D. Aagaard) Date: Mon, 19 Apr 1993 10:09:39 -0400 Organization: Cornell University, Electrical Engineering, Ithaca NY 14853 X-Address: 389 Engineering and Theory Center X-Phone: (607) 255 0302 X-Fax: (607) 255 9072 X-Mailer: Mail User's Shell (7.2.4 2/2/92) To: info-hol@ted.cs.uidaho.edu Subject: discrimination nets A few days ago Tom Melham mentioned that HOL uses discrimination nets in rewriting. Is there any documentation describing the use of discrimination nets in rewriting, or could someone point out a good paper on them? Thanks in advance, mark aagaard markaa@ee.cornell.edu