author | nipkow |
Fri, 04 Apr 1997 14:48:40 +0200 | |
changeset 2903 | d1d5a0acbf72 |
parent 1476 | 608483c2122a |
child 3192 | a75558a4ed37 |
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 b (split c) al" assoc_def "assoc v d al == alist_rec al d (%x y xs g.if v=x then y else g)" end