# HG changeset patch
# User paulson
# Date 992068926 -7200
# Node ID 01020b10c0a71d498db239c8823d2cf192b70526
# Parent  a548865b1b6abcd91eab6e5067591b5ef6838406
simplified a proof using new dvd rules

diff -r a548865b1b6a -r 01020b10c0a7 src/HOL/IMPP/EvenOdd.ML
--- a/src/HOL/IMPP/EvenOdd.ML	Sat Jun 09 08:41:25 2001 +0200
+++ b/src/HOL/IMPP/EvenOdd.ML	Sat Jun 09 08:42:06 2001 +0200
@@ -12,9 +12,7 @@
 Addsimps [even_0];
 
 Goalw [even_def] "even 1 = False";
-by (Clarsimp_tac 1);
-by (dtac dvd_imp_le 1);
-by Auto_tac;
+by (Simp_tac 1);
 qed "not_even_1";
 Addsimps [not_even_1];
 
diff -r a548865b1b6a -r 01020b10c0a7 src/HOL/NumberTheory/Factorization.thy
--- a/src/HOL/NumberTheory/Factorization.thy	Sat Jun 09 08:41:25 2001 +0200
+++ b/src/HOL/NumberTheory/Factorization.thy	Sat Jun 09 08:42:06 2001 +0200
@@ -258,11 +258,8 @@
 lemma prime_dvd_mult_list [rule_format]:
     "p \<in> prime ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> p dvd m)"
   apply (induct xs)
-   apply simp_all
-   apply (erule prime_nd_one)
-  apply (rule impI)
-  apply (drule prime_dvd_mult)
-   apply auto
+   apply (force simp add: prime_def)
+   apply (force dest: prime_dvd_mult)
   done
 
 lemma hd_xs_dvd_prod: