--- a/Quot/QuotList.thy	Tue Jan 26 10:53:44 2010 +0100
+++ b/Quot/QuotList.thy	Tue Jan 26 11:13:08 2010 +0100
@@ -1,7 +1,12 @@
- theory QuotList
+(*  Title:      QuotList.thy
+    Author:     Cezary Kaliszyk and Christian Urban
+*) 
+theory QuotList
 imports QuotMain List
 begin
 
+section {* Quotient infrastructure for the list type. *}
+
 fun
   list_rel
 where
@@ -12,9 +17,6 @@
 
 declare [[map list = (map, list_rel)]]
 
-
-
-text {* should probably be in Sum_Type.thy *}
 lemma split_list_all: 
   shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))"
   apply(auto)