author | clasohm |
Wed, 02 Mar 1994 12:26:55 +0100 | |
changeset 48 | 21291189b51e |
parent 0 | 7949f97df77a |
permissions | -rw-r--r-- |
(* Title: Substitutions/alist.thy Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Association lists. *) AList = List + consts alist_rec :: "[('a*'b) list,'c,['a,'b,('a*'b) list,'c]=>'c]=>'c" assoc :: "['a,'b,('a*'b) list] => 'b" rules alist_rec_def "alist_rec(al,b,c) == list_rec(al,b,%p xs g.split(p,%x y.c(x,y,xs,g)))" assoc_def "assoc(v,d,al) == alist_rec(al,d,%x y xs g.if(v=x,y,g))" end