--- a/QuotList.thy	Fri Dec 04 15:04:05 2009 +0100
+++ b/QuotList.thy	Fri Dec 04 15:18:33 2009 +0100
@@ -2,7 +2,7 @@
 imports QuotScript
 begin
 
-lemma LIST_map_I:
+lemma LIST_map_id:
   shows "map (\<lambda>x. x) = (\<lambda>x. x)"
   by simp
 
@@ -28,10 +28,10 @@
   shows "LIST_REL R x x"
 by (induct x) (auto simp add: a)
 
-lemma LIST_EQUIV:
-  assumes a: "EQUIV R"
-  shows "EQUIV (LIST_REL R)"
-unfolding EQUIV_def
+lemma LIST_equivp:
+  assumes a: "equivp R"
+  shows "equivp (LIST_REL R)"
+unfolding equivp_def
 apply(rule allI)+
 apply(induct_tac x y rule: list_induct2')
 apply(simp)
@@ -46,70 +46,70 @@
 apply(simp)
 apply(simp)
 using a
-apply(unfold EQUIV_def)
+apply(unfold equivp_def)
 apply(auto)[1]
 apply(metis LIST_REL.simps(4))
 done
 
 lemma LIST_REL_REL: 
-  assumes q: "QUOTIENT R Abs Rep"
+  assumes q: "Quotient R Abs Rep"
   shows "LIST_REL R r s = (LIST_REL R r r \<and> LIST_REL R s s \<and> (map Abs r = map Abs s))"
 apply(induct r s rule: list_induct2')
 apply(simp_all)
-using QUOTIENT_REL[OF q]
+using Quotient_REL[OF q]
 apply(metis)
 done
 
-lemma LIST_QUOTIENT:
-  assumes q: "QUOTIENT R Abs Rep"
-  shows "QUOTIENT (LIST_REL R) (map Abs) (map Rep)"
-unfolding QUOTIENT_def
+lemma LIST_Quotient:
+  assumes q: "Quotient R Abs Rep"
+  shows "Quotient (LIST_REL R) (map Abs) (map Rep)"
+unfolding Quotient_def
 apply(rule conjI)
 apply(rule allI)
 apply(induct_tac a)
 apply(simp)
-apply(simp add: QUOTIENT_ABS_REP[OF q])
+apply(simp add: Quotient_ABS_REP[OF q])
 apply(rule conjI)
 apply(rule allI)
 apply(induct_tac a)
 apply(simp)
 apply(simp)
-apply(simp add: QUOTIENT_REP_REFL[OF q])
+apply(simp add: Quotient_REP_reflp[OF q])
 apply(rule allI)+
 apply(rule LIST_REL_REL[OF q])
 done
 
 lemma CONS_PRS:
-  assumes q: "QUOTIENT R Abs Rep"
+  assumes q: "Quotient R Abs Rep"
   shows "(h#t) = (map Abs) ((Rep h)#(map Rep t))"
-by (induct t) (simp_all add: QUOTIENT_ABS_REP[OF q])
+by (induct t) (simp_all add: Quotient_ABS_REP[OF q])
 
 lemma CONS_RSP:
-  assumes q: "QUOTIENT R Abs Rep"
+  assumes q: "Quotient R Abs Rep"
   and     a: "R h1 h2" "LIST_REL R t1 t2"
   shows "LIST_REL R (h1#t1) (h2#t2)"
 using a by (auto)
 
 lemma NIL_PRS:
-  assumes q: "QUOTIENT R Abs Rep"
+  assumes q: "Quotient R Abs Rep"
   shows "[] = (map Abs [])"
 by (simp)
 
 lemma NIL_RSP:
-  assumes q: "QUOTIENT R Abs Rep"
+  assumes q: "Quotient R Abs Rep"
   shows "LIST_REL R [] []"
 by simp
 
 lemma MAP_PRS:
-  assumes q1: "QUOTIENT R1 Abs1 Rep1"
-  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  and     q2: "Quotient R2 Abs2 Rep2"
   shows "map f l = (map Abs2) (map ((Abs1 ---> Rep2) f) (map Rep1 l))"
 by (induct l)
-   (simp_all add: QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2])
+   (simp_all add: Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2])
 
 lemma MAP_RSP:
-  assumes q1: "QUOTIENT R1 Abs1 Rep1"
-  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  and     q2: "Quotient R2 Abs2 Rep2"
   and     a: "(R1 ===> R2) f1 f2" 
   and     b: "LIST_REL R1 l1 l2"
   shows "LIST_REL R2 (map f1 l1) (map f2 l2)"