src/HOL/Subst/AList.thy
changeset 968 3cdaa8724175
child 1476 608483c2122a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Subst/AList.thy	Tue Mar 21 13:22:28 1995 +0100
     1.3 @@ -0,0 +1,21 @@
     1.4 +(*  Title: 	Substitutions/alist.thy
     1.5 +    Author: 	Martin Coen, Cambridge University Computer Laboratory
     1.6 +    Copyright   1993  University of Cambridge
     1.7 +
     1.8 +Association lists.
     1.9 +*)
    1.10 +
    1.11 +AList = List + 
    1.12 +
    1.13 +consts
    1.14 +
    1.15 +  alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
    1.16 +  assoc      :: "['a,'b,('a*'b) list] => 'b"
    1.17 +
    1.18 +rules
    1.19 +
    1.20 +  alist_rec_def "alist_rec al b c == list_rec b (split c) al"
    1.21 +
    1.22 +  assoc_def   "assoc v d al == alist_rec al d (%x y xs g.if v=x then y else g)"
    1.23 +
    1.24 +end