isabelle: src/HOL/Subst/AList.thy@0a22b9d63a18 (annotated)

1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 968 diff changeset	1	(* Title: Substitutions/alist.thy
608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 968 diff changeset	2	Author: Martin Coen, Cambridge University Computer Laboratory
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	3	Copyright 1993 University of Cambridge
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	4
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	5	Association lists.
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	6	*)
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	7
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	8	AList = List +
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	9
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	10	consts
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	11
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
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	15	rules
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	16
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	17	alist_rec_def "alist_rec al b c == list_rec b (split c) al"
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	18
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	19	assoc_def "assoc v d al == alist_rec al d (%x y xs g.if v=x then y else g)"
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	20
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	21	end

author	paulson
	Mon, 23 Sep 1996 18:18:18 +0200
changeset 2010	0a22b9d63a18
parent 1476	608483c2122a
child 3192	a75558a4ed37
permissions	-rw-r--r--