diff -r 820c64273ce0 -r 5cb44fe9ae8e Quot/QuotList.thy
--- a/Quot/QuotList.thy	Tue Dec 08 17:35:04 2009 +0100
+++ b/Quot/QuotList.thy	Tue Dec 08 17:39:34 2009 +0100
@@ -12,7 +12,7 @@
 
 declare [[map list = (map, list_rel)]]
 
-lemma list_equivp[quotient_equiv]:
+lemma list_equivp[quot_equiv]:
   assumes a: "equivp R"
   shows "equivp (list_rel R)"
   unfolding equivp_def
@@ -40,7 +40,7 @@
   apply(metis)
   done
 
-lemma list_quotient[quotient_thm]:
+lemma list_quotient[quot_thm]:
   assumes q: "Quotient R Abs Rep"
   shows "Quotient (list_rel R) (map Abs) (map Rep)"
   unfolding Quotient_def
@@ -72,7 +72,7 @@
   shows "(map Abs) ((Rep h) # (map Rep t)) = h # t"
 by (induct t) (simp_all add: Quotient_abs_rep[OF q])
 
-lemma cons_rsp[quotient_rsp]:
+lemma cons_rsp[quot_respect]:
   assumes q: "Quotient R Abs Rep"
   shows "(R ===> list_rel R ===> list_rel R) op # op #"
 by (auto)
@@ -82,7 +82,7 @@
   shows "map Abs [] \<equiv> []"
 by (simp)
 
-lemma nil_rsp[quotient_rsp]:
+lemma nil_rsp[quot_respect]:
   assumes q: "Quotient R Abs Rep"
   shows "list_rel R [] []"
 by simp
@@ -93,7 +93,7 @@
   shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
 
-lemma map_rsp[quotient_rsp]:
+lemma map_rsp[quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map"
@@ -131,7 +131,7 @@
          induct     doesn't accept 'rule'.
    that's why the proof uses manual generalisation and needs assumptions
    both in conclusion for induction and in assumptions. *)
-lemma foldl_rsp[quotient_rsp]:
+lemma foldl_rsp[quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl"