src/HOL/Library/Primes.thy
changeset 26159 ff372ff5cc34
parent 26144 98d23fc02585
child 26757 e775accff967
     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