diff -r 000000000000 -r 7949f97df77a Subst/AList.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Subst/AList.thy	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,22 @@
+(*  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