# HG changeset patch
# User wenzelm
# Date 1015433683 -3600
# Node ID 1ec445c51931bd8db537011b7c420c0024a5c8ff
# Parent  3f7824dd8ddf6ddc82b630935c35800a558e196c
added two_is_prime;

diff -r 3f7824dd8ddf -r 1ec445c51931 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