author | chaieb |
Wed, 27 Feb 2008 14:39:54 +0100 | |
changeset 26159 | ff372ff5cc34 |
parent 26158 | 9dc286ee452b |
child 26160 | ff5bb2b532b3 |
1.1 --- a/src/HOL/Library/Primes.thy Wed Feb 27 14:39:52 2008 +0100 1.2 +++ b/src/HOL/Library/Primes.thy Wed Feb 27 14:39:54 2008 +0100 1.3 @@ -1043,4 +1043,6 @@ 1.4 lemma coprime_divisors: "d dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> coprime d e" 1.5 by (auto simp add: dvd_def coprime) 1.6 1.7 +declare power_Suc0[simp del] 1.8 +declare even_dvd[simp del] 1.9 end