isabelle: src/Pure/net.ML@8d8c70b41bab (annotated)

12319 cb3ea5750c3b most general type of delete/delete_term; wenzelm parents: 7943 diff changeset	1	(* Title: Pure/net.ML
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
12319 cb3ea5750c3b most general type of delete/delete_term; wenzelm parents: 7943 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
a5a9c433f639 Initial revision clasohm parents: diff changeset	6	Discrimination nets: a data structure for indexing items
a5a9c433f639 Initial revision clasohm parents: diff changeset	7
12319 cb3ea5750c3b most general type of delete/delete_term; wenzelm parents: 7943 diff changeset	8	From the book
cb3ea5750c3b most general type of delete/delete_term; wenzelm parents: 7943 diff changeset	9	E. Charniak, C. K. Riesbeck, D. V. McDermott.
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	10	Artificial Intelligence Programming.
a5a9c433f639 Initial revision clasohm parents: diff changeset	11	(Lawrence Erlbaum Associates, 1980). [Chapter 14]
225 76f60e6400e8 optimized net for matching of abstractions to speed up simplifier nipkow parents: 0 diff changeset	12
12319 cb3ea5750c3b most general type of delete/delete_term; wenzelm parents: 7943 diff changeset	13	match_term no longer treats abstractions as wildcards; instead they match
228 4f43430f226e some optimizations of Larry's nipkow parents: 225 diff changeset	14	only wildcards in patterns. Requires operands to be beta-eta-normal.
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	15	*)
a5a9c433f639 Initial revision clasohm

author	skalberg
	Thu, 03 Mar 2005 12:43:01 +0100
changeset 15570	8d8c70b41bab
parent 12319	cb3ea5750c3b
child 15574	b1d1b5bfc464
permissions	-rw-r--r--