tuned proofs
authorbulwahn
Thu Nov 08 20:02:41 2012 +0100 (2012-11-08)
changeset 50037f2a32197a33a
parent 50036 aa83d943c18b
child 50038 8e32c9254535
tuned proofs
src/HOL/Algebra/Divisibility.thy
src/HOL/Library/Permutation.thy
src/HOL/Old_Number_Theory/Primes.thy
     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Thu Nov 08 19:55:37 2012 +0100
     1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Thu Nov 08 20:02:41 2012 +0100
     1.3 @@ -244,7 +244,7 @@
     1.4   apply (elim dividesE, intro dividesI, assumption)
     1.5   apply (rule l_cancel[of c])
     1.6      apply (simp add: m_assoc carr)+
     1.7 -apply (fast intro: divides_mult_lI carr)
     1.8 +apply (fast intro: carr)
     1.9  done
    1.10  
    1.11  lemma (in comm_monoid) divides_mult_rI [intro]:
     2.1 --- a/src/HOL/Library/Permutation.thy	Thu Nov 08 19:55:37 2012 +0100
     2.2 +++ b/src/HOL/Library/Permutation.thy	Thu Nov 08 20:02:41 2012 +0100
     2.3 @@ -193,7 +193,7 @@
     2.4    show ?case
     2.5    proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI)
     2.6      show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
     2.7 -      by (auto simp: bij_betw_def bij_betw_swap_iff)
     2.8 +      by (auto simp: bij_betw_def)
     2.9      fix i assume "i < length(y#x#l)"
    2.10      show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
    2.11        by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
     3.1 --- a/src/HOL/Old_Number_Theory/Primes.thy	Thu Nov 08 19:55:37 2012 +0100
     3.2 +++ b/src/HOL/Old_Number_Theory/Primes.thy	Thu Nov 08 20:02:41 2012 +0100
     3.3 @@ -24,7 +24,7 @@
     3.4  
     3.5  lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd p n = 1"
     3.6    apply (auto simp add: prime_def)
     3.7 -  apply (metis One_nat_def gcd_dvd1 gcd_dvd2)
     3.8 +  apply (metis gcd_dvd1 gcd_dvd2)
     3.9    done
    3.10  
    3.11  text {*