# HG changeset patch
# User nipkow
# Date 1248166867 -7200
# Node ID 7c39fcfffd6172937cd321c5e320cd9bafceb65b
# Parent  2110fcd86efbea48f4ab5bbcc97d620c547d4695
Tests for executability of "prime"

diff -r 2110fcd86efb -r 7c39fcfffd61 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Mon Jul 20 20:03:19 2009 +0200
+++ b/src/HOL/GCD.thy	Tue Jul 21 11:01:07 2009 +0200
@@ -1657,6 +1657,20 @@
 lemma two_is_prime_int [simp]: "prime (2::int)"
 by simp
 
+text{* A bit of regression testing: *}
+
+lemma "prime(97::nat)"
+by simp
+
+lemma "prime(97::int)"
+by simp
+
+lemma "prime(997::nat)"
+by eval
+
+lemma "prime(997::int)"
+by eval
+
 
 lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   apply (rule coprime_exp_nat)