src/HOL/GCD.thy
changeset 29700 22faf21db3df
parent 29655 ac31940cfb69
child 30042 31039ee583fa
child 30240 5b25fee0362c
     1.1 --- a/src/HOL/GCD.thy	Fri Jan 30 13:41:45 2009 +0000
     1.2 +++ b/src/HOL/GCD.thy	Sat Jan 31 09:04:16 2009 +0100
     1.3 @@ -562,25 +562,25 @@
     1.4    "zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))"
     1.5  
     1.6  lemma zgcd_zdvd1 [iff,simp, algebra]: "zgcd i j dvd i"
     1.7 -  by (simp add: zgcd_def int_dvd_iff)
     1.8 +by (simp add: zgcd_def int_dvd_iff)
     1.9  
    1.10  lemma zgcd_zdvd2 [iff,simp, algebra]: "zgcd i j dvd j"
    1.11 -  by (simp add: zgcd_def int_dvd_iff)
    1.12 +by (simp add: zgcd_def int_dvd_iff)
    1.13  
    1.14  lemma zgcd_pos: "zgcd i j \<ge> 0"
    1.15 -  by (simp add: zgcd_def)
    1.16 +by (simp add: zgcd_def)
    1.17  
    1.18  lemma zgcd0 [simp,algebra]: "(zgcd i j = 0) = (i = 0 \<and> j = 0)"
    1.19 -  by (simp add: zgcd_def gcd_zero) arith
    1.20 +by (simp add: zgcd_def gcd_zero)
    1.21  
    1.22  lemma zgcd_commute: "zgcd i j = zgcd j i"
    1.23 -  unfolding zgcd_def by (simp add: gcd_commute)
    1.24 +unfolding zgcd_def by (simp add: gcd_commute)
    1.25  
    1.26  lemma zgcd_zminus [simp, algebra]: "zgcd (- i) j = zgcd i j"
    1.27 -  unfolding zgcd_def by simp
    1.28 +unfolding zgcd_def by simp
    1.29  
    1.30  lemma zgcd_zminus2 [simp, algebra]: "zgcd i (- j) = zgcd i j"
    1.31 -  unfolding zgcd_def by simp
    1.32 +unfolding zgcd_def by simp
    1.33  
    1.34    (* should be solved by algebra*)
    1.35  lemma zrelprime_dvd_mult: "zgcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"