diff -r f04b33ce250f -r a4dc62a46ee4 Subst/AList.thy --- a/Subst/AList.thy Tue Oct 24 14:59:17 1995 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ -(* 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,y,g))" - -end