src/HOL/Subst/AList.thy
author clasohm
Tue Mar 21 13:22:28 1995 +0100 (1995-03-21)
changeset 968 3cdaa8724175
child 1476 608483c2122a
permissions -rw-r--r--
converted Subst with curried function application
     1 (*  Title: 	Substitutions/alist.thy
     2     Author: 	Martin Coen, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 
     5 Association lists.
     6 *)
     7 
     8 AList = List + 
     9 
    10 consts
    11 
    12   alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
    13   assoc      :: "['a,'b,('a*'b) list] => 'b"
    14 
    15 rules
    16 
    17   alist_rec_def "alist_rec al b c == list_rec b (split c) al"
    18 
    19   assoc_def   "assoc v d al == alist_rec al d (%x y xs g.if v=x then y else g)"
    20 
    21 end