diff -r bca33c49b083 -r 8408a06590a6 src/HOL/Subst/AList.thy
--- a/src/HOL/Subst/AList.thy	Mon Mar 28 16:19:56 2005 +0200
+++ b/src/HOL/Subst/AList.thy	Tue Mar 29 12:30:48 2005 +0200
@@ -1,12 +1,14 @@
-(*  Title:      Subst/AList.thy
-    ID:         $Id$
+(*  ID:         $Id$
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Association lists.
 *)
 
-AList = Main +
+header{*Association Lists*}
+
+theory AList
+imports Main
+begin
 
 consts
   alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
@@ -20,4 +22,10 @@
   "assoc v d [] = d"
   "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
 
+
+lemma alist_induct:
+    "[| P([]);    
+        !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)"
+by (induct_tac "l", auto)
+
 end