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