--- a/Quot/Examples/IntEx2.thy	Tue Dec 08 16:36:01 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Tue Dec 08 17:30:00 2009 +0100
@@ -107,21 +107,21 @@
 
 thm add_assoc
 
-lemma plus_raw_rsp[quotient_rsp]:
+lemma plus_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
 by auto
 
-lemma minus_raw_rsp[quotient_rsp]:
+lemma minus_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx>) minus_raw minus_raw"
   by auto
 
-lemma mult_raw_rsp[quotient_rsp]:
+lemma mult_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
 apply(auto)
 apply(simp add: algebra_simps)
 sorry
 
-lemma le_raw_rsp[quotient_rsp]:
+lemma le_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"
 by auto