# HG changeset patch
# User bulwahn
# Date 1352401361 -3600
# Node ID f2a32197a33a38984114b9a5d1a4ff660f393a20
# Parent  aa83d943c18bc9a8753b99b30ad159d4f9104294
tuned proofs

diff -r aa83d943c18b -r f2a32197a33a src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Thu Nov 08 19:55:37 2012 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Thu Nov 08 20:02:41 2012 +0100
@@ -244,7 +244,7 @@
  apply (elim dividesE, intro dividesI, assumption)
  apply (rule l_cancel[of c])
     apply (simp add: m_assoc carr)+
-apply (fast intro: divides_mult_lI carr)
+apply (fast intro: carr)
 done
 
 lemma (in comm_monoid) divides_mult_rI [intro]:
diff -r aa83d943c18b -r f2a32197a33a src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Thu Nov 08 19:55:37 2012 +0100
+++ b/src/HOL/Library/Permutation.thy	Thu Nov 08 20:02:41 2012 +0100
@@ -193,7 +193,7 @@
   show ?case
   proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI)
     show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
-      by (auto simp: bij_betw_def bij_betw_swap_iff)
+      by (auto simp: bij_betw_def)
     fix i assume "i < length(y#x#l)"
     show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
       by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
diff -r aa83d943c18b -r f2a32197a33a src/HOL/Old_Number_Theory/Primes.thy
--- a/src/HOL/Old_Number_Theory/Primes.thy	Thu Nov 08 19:55:37 2012 +0100
+++ b/src/HOL/Old_Number_Theory/Primes.thy	Thu Nov 08 20:02:41 2012 +0100
@@ -24,7 +24,7 @@
 
 lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd p n = 1"
   apply (auto simp add: prime_def)
-  apply (metis One_nat_def gcd_dvd1 gcd_dvd2)
+  apply (metis gcd_dvd1 gcd_dvd2)
   done
 
 text {*