Subst/AList.thy
changeset 252 a4dc62a46ee4
parent 251 f04b33ce250f
child 253 132634d24019
--- 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