isabelle: src/HOL/Subst/AList.thy@b3e39a2987c1 (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
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	9	AList = List +
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
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	13	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	14	assoc :: "['a,'b,('a*'b) list] => 'b"
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	15
3192 a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1476 diff changeset	16	defs
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	17
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	18	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	19
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	20	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	21
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	22	end

author	paulson
	Mon, 26 May 1997 12:40:51 +0200
changeset 3344	b3e39a2987c1
parent 3268	012c43174664
child 3842	b55686a7b22c
permissions	-rw-r--r--