src/HOL/Subst/AList.thy
author clasohm
Mon Feb 05 21:29:06 1996 +0100 (1996-02-05)
changeset 1476 608483c2122a
parent 968 3cdaa8724175
child 3192 a75558a4ed37
permissions -rw-r--r--
expanded tabs; incorporated Konrad's changes
clasohm@1476
     1
(*  Title:      Substitutions/alist.thy
clasohm@1476
     2
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@968
     3
    Copyright   1993  University of Cambridge
clasohm@968
     4
clasohm@968
     5
Association lists.
clasohm@968
     6
*)
clasohm@968
     7
clasohm@968
     8
AList = List + 
clasohm@968
     9
clasohm@968
    10
consts
clasohm@968
    11
clasohm@968
    12
  alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
clasohm@968
    13
  assoc      :: "['a,'b,('a*'b) list] => 'b"
clasohm@968
    14
clasohm@968
    15
rules
clasohm@968
    16
clasohm@968
    17
  alist_rec_def "alist_rec al b c == list_rec b (split c) al"
clasohm@968
    18
clasohm@968
    19
  assoc_def   "assoc v d al == alist_rec al d (%x y xs g.if v=x then y else g)"
clasohm@968
    20
clasohm@968
    21
end