fun_rel_def is no simp rule by default

--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Tue Nov 09 14:02:13 2010 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Tue Nov 09 14:02:14 2010 +0100
@@ -77,7 +77,7 @@
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_int_raw plus_int_raw"
   and   "(op \<approx> ===> op \<approx>) uminus_int_raw uminus_int_raw"
   and   "(op \<approx> ===> op \<approx> ===> op =) le_int_raw le_int_raw"
-  by auto
+  by (auto intro!: fun_relI)
 
 lemma times_int_raw_fst:
   assumes a: "x \<approx> z"
@@ -167,7 +167,7 @@
 
 lemma[quot_respect]:
   shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
-  by (simp add: equivp_reflp[OF int_equivp])
+  by (auto simp add: equivp_reflp [OF int_equivp])
 
 lemma int_of_nat:
   shows "of_nat m = int_of_nat m"

--- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Nov 09 14:02:13 2010 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Nov 09 14:02:14 2010 +0100
@@ -179,11 +179,11 @@
 
 lemma [quot_respect]:
   shows "(op \<sim> ===> op =) freenonces freenonces"
-  by (simp add: msgrel_imp_eq_freenonces)
+  by (auto simp add: msgrel_imp_eq_freenonces)
 
 lemma [quot_respect]:
   shows "(op = ===> op \<sim>) NONCE NONCE"
-  by (simp add: NONCE)
+  by (auto simp add: NONCE)
 
 lemma nonces_Nonce [simp]:
   shows "nonces (Nonce N) = {N}"
@@ -191,7 +191,7 @@
 
 lemma [quot_respect]:
   shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
-  by (simp add: MPAIR)
+  by (auto simp add: MPAIR)
 
 lemma nonces_MPair [simp]:
   shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
@@ -214,7 +214,7 @@
 
 lemma [quot_respect]:
   shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
-  by (simp add: msgrel_imp_eqv_freeleft)
+  by (auto simp add: msgrel_imp_eqv_freeleft)
 
 lemma left_Nonce [simp]:
   shows "left (Nonce N) = Nonce N"
@@ -243,7 +243,7 @@
 
 lemma [quot_respect]:
   shows "(op \<sim> ===> op \<sim>) freeright freeright"
-  by (simp add: msgrel_imp_eqv_freeright)
+  by (auto simp add: msgrel_imp_eqv_freeright)
 
 lemma right_Nonce [simp]:
   shows "right (Nonce N) = Nonce N"