src/HOL/NumberTheory/Factorization.thy
changeset 11364 01020b10c0a7
parent 11049 7eef34adb852
child 11468 02cd5d5bc497
     1.1 --- a/src/HOL/NumberTheory/Factorization.thy	Sat Jun 09 08:41:25 2001 +0200
     1.2 +++ b/src/HOL/NumberTheory/Factorization.thy	Sat Jun 09 08:42:06 2001 +0200
     1.3 @@ -258,11 +258,8 @@
     1.4  lemma prime_dvd_mult_list [rule_format]:
     1.5      "p \<in> prime ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> p dvd m)"
     1.6    apply (induct xs)
     1.7 -   apply simp_all
     1.8 -   apply (erule prime_nd_one)
     1.9 -  apply (rule impI)
    1.10 -  apply (drule prime_dvd_mult)
    1.11 -   apply auto
    1.12 +   apply (force simp add: prime_def)
    1.13 +   apply (force dest: prime_dvd_mult)
    1.14    done
    1.15  
    1.16  lemma hd_xs_dvd_prod: