src/HOL/Subst/AList.thy
author clasohm
Wed Mar 13 11:55:25 1996 +0100 (1996-03-13 ago)
changeset 1574 5a63ab90ee8a
parent 1476 608483c2122a
child 3192 a75558a4ed37
permissions -rw-r--r--
modified primrec so it can be used in MiniML/Type.thy
     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