--- 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"