isabelle: src/HOL/Subst/AList.thy@6123bfc55247 (annotated)

3268 012c43174664 Mostly cosmetic changes: updated headers, ID lines, etc. paulson parents: 3192 diff changeset	1	(* Title: Subst/AList.thy
012c43174664 Mostly cosmetic changes: updated headers, ID lines, etc. paulson parents: 3192 diff changeset	2	ID: $Id$
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 968 diff changeset	3	Author: Martin Coen, Cambridge University Computer Laboratory
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	5
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	6	Association lists.
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	7	*)
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	8
12406 c9775847ed66 use Main; wenzelm parents: 8874 diff changeset	9	AList = Main +
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	10
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	11	consts
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	12	alist_rec :: "[('a'b)list, 'c, ['a, 'b, ('a'b)list, 'c]=>'c] => 'c"
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	13	assoc :: "['a,'b,('a*'b) list] => 'b"
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	14
8874 3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	15	primrec
3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	16	"alist_rec [] c d = c"
3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	17	"alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	18
8874 3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	19	primrec
3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	20	"assoc v d [] = d"
3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	21	"assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	22
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	23	end

author	paulson
	Tue, 27 May 2003 11:46:29 +0200
changeset 14047	6123bfc55247
parent 12406	c9775847ed66
child 15635	8408a06590a6
permissions	-rw-r--r--