src/HOL/Subst/AList.thy
author wenzelm
Fri Oct 10 19:02:28 1997 +0200 (1997-10-10)
changeset 3842 b55686a7b22c
parent 3268 012c43174664
child 8874 3242637f668c
permissions -rw-r--r--
fixed dots;
     1 (*  Title:      Subst/AList.thy
     2     ID:         $Id$
     3     Author:     Martin Coen, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Association lists.
     7 *)
     8 
     9 AList = List + 
    10 
    11 consts
    12 
    13   alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
    14   assoc      :: "['a,'b,('a*'b) list] => 'b"
    15 
    16 defs
    17 
    18   alist_rec_def "alist_rec al b c == list_rec b (split c) al"
    19 
    20   assoc_def   "assoc v d al == alist_rec al d (%x y xs g. if v=x then y else g)"
    21 
    22 end