Old_HOL: Subst/AList.thy@0f9230a24164 (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
194 b93cc55cb7ab small updates because datatype list is now used. In particular Nil -> [] nipkow parents: 106 diff changeset	17	alist_rec_def "alist_rec(al,b,c) == list_rec(b, split(c), al)"
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	lcp
	Thu, 06 Apr 1995 11:49:42 +0200
changeset 246	0f9230a24164
parent 194	b93cc55cb7ab
permissions	-rw-r--r--