src/HOL/Library/Primes.thy

--- a/src/HOL/Library/Primes.thy	Wed Mar 06 17:48:39 2002 +0100
+++ b/src/HOL/Library/Primes.thy	Wed Mar 06 17:54:43 2002 +0100
@@ -181,6 +181,13 @@
   apply simp
   done
 
+lemma two_is_prime: "2 \<in> prime"
+  apply (auto simp add: prime_def)
+  apply (case_tac m)
+   apply (auto dest!: dvd_imp_le)
+  apply arith
+  done
+
 text {*
   This theorem leads immediately to a proof of the uniqueness of
   factorization.  If @{term p} divides a product of primes then it is