isabelle: src/HOL/Subst/AList.thy@74919e8f221c (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
3842 b55686a7b22c fixed dots; wenzelm parents: 3268 diff changeset	20	assoc_def "assoc v d al == alist_rec al d (%x y xs g. if v=x then y else g)"
968 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
	Wed, 15 Jul 1998 14:19:02 +0200
changeset 5148	74919e8f221c
parent 3842	b55686a7b22c
child 8874	3242637f668c
permissions	-rw-r--r--