Old_HOL: Subst/AList.thy@fd1be45b64bf (annotated)

0 7949f97df77a Initial revision clasohm parents: diff changeset	1	(* Title: Substitutions/alist.thy
7949f97df77a Initial revision clasohm parents: diff changeset	2	Author: Martin Coen, Cambridge University Computer Laboratory
7949f97df77a Initial revision clasohm parents: diff changeset	3	Copyright 1993 University of Cambridge
7949f97df77a Initial revision clasohm parents: diff changeset	4
7949f97df77a Initial revision clasohm parents: diff changeset	5	Association lists.
7949f97df77a Initial revision clasohm parents: diff changeset	6	*)
7949f97df77a Initial revision clasohm parents: diff changeset	7
7949f97df77a Initial revision clasohm parents: diff changeset	8	AList = List +
7949f97df77a Initial revision clasohm parents: diff changeset	9
7949f97df77a Initial revision clasohm parents: diff changeset	10	consts
7949f97df77a Initial revision clasohm parents: diff changeset	11
106 d27056ec0a5a HOL/Subst/AList: swapped args of split and simplified lcp parents: 0 diff changeset	12	alist_rec :: "[('a'b)list, 'c, ['a, 'b, ('a'b)list, 'c]=>'c] => 'c"
0 7949f97df77a Initial revision clasohm parents: diff changeset	13	assoc :: "['a,'b,('a*'b) list] => 'b"
7949f97df77a Initial revision clasohm parents: diff changeset	14
7949f97df77a Initial revision clasohm parents: diff changeset	15	rules
7949f97df77a Initial revision clasohm parents: diff changeset	16
106 d27056ec0a5a HOL/Subst/AList: swapped args of split and simplified lcp parents: 0 diff changeset	17	alist_rec_def "alist_rec(al,b,c) == list_rec(al, b, split(c))"
0 7949f97df77a Initial revision clasohm parents: diff changeset	18
106 d27056ec0a5a HOL/Subst/AList: swapped args of split and simplified lcp parents: 0 diff changeset	19	assoc_def "assoc(v,d,al) == alist_rec(al,d,%x y xs g.if(v=x,y,g))"
0 7949f97df77a Initial revision clasohm parents: diff changeset	20
7949f97df77a Initial revision clasohm parents: diff changeset	21	end

author	clasohm
	Wed, 02 Nov 1994 11:50:09 +0100
changeset 156	fd1be45b64bf
parent 106	d27056ec0a5a
child 194	b93cc55cb7ab
permissions	-rw-r--r--