author | clasohm |
Tue, 21 Mar 1995 13:22:28 +0100 | |
changeset 968 | 3cdaa8724175 |
child 1476 | 608483c2122a |
permissions | -rw-r--r-- |
968 | 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 |