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;
paulson@3268
     1
(*  Title:      Subst/AList.thy
paulson@3268
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@968
     4
    Copyright   1993  University of Cambridge
clasohm@968
     5
clasohm@968
     6
Association lists.
clasohm@968
     7
*)
clasohm@968
     8
clasohm@968
     9
AList = List + 
clasohm@968
    10
clasohm@968
    11
consts
clasohm@968
    12
clasohm@968
    13
  alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
clasohm@968
    14
  assoc      :: "['a,'b,('a*'b) list] => 'b"
clasohm@968
    15
paulson@3192
    16
defs
clasohm@968
    17
clasohm@968
    18
  alist_rec_def "alist_rec al b c == list_rec b (split c) al"
clasohm@968
    19
wenzelm@3842
    20
  assoc_def   "assoc v d al == alist_rec al d (%x y xs g. if v=x then y else g)"
clasohm@968
    21
clasohm@968
    22
end