author | paulson |
Tue, 23 May 2000 18:06:22 +0200 | |
changeset 8935 | 548901d05a0e |
parent 8874 | 3242637f668c |
child 12406 | c9775847ed66 |
permissions | -rw-r--r-- |
(* Title: Subst/AList.thy ID: $Id$ 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" primrec "alist_rec [] c d = c" "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)" primrec "assoc v d [] = d" "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)" end