simplified a proof using new dvd rules
authorpaulson
Sat Jun 09 08:42:06 2001 +0200 (2001-06-09)
changeset 1136401020b10c0a7
parent 11363 a548865b1b6a
child 11365 6d5698df0413
simplified a proof using new dvd rules
src/HOL/IMPP/EvenOdd.ML
src/HOL/NumberTheory/Factorization.thy
     1.1 --- a/src/HOL/IMPP/EvenOdd.ML	Sat Jun 09 08:41:25 2001 +0200
     1.2 +++ b/src/HOL/IMPP/EvenOdd.ML	Sat Jun 09 08:42:06 2001 +0200
     1.3 @@ -12,9 +12,7 @@
     1.4  Addsimps [even_0];
     1.5  
     1.6  Goalw [even_def] "even 1 = False";
     1.7 -by (Clarsimp_tac 1);
     1.8 -by (dtac dvd_imp_le 1);
     1.9 -by Auto_tac;
    1.10 +by (Simp_tac 1);
    1.11  qed "not_even_1";
    1.12  Addsimps [not_even_1];
    1.13  
     2.1 --- a/src/HOL/NumberTheory/Factorization.thy	Sat Jun 09 08:41:25 2001 +0200
     2.2 +++ b/src/HOL/NumberTheory/Factorization.thy	Sat Jun 09 08:42:06 2001 +0200
     2.3 @@ -258,11 +258,8 @@
     2.4  lemma prime_dvd_mult_list [rule_format]:
     2.5      "p \<in> prime ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> p dvd m)"
     2.6    apply (induct xs)
     2.7 -   apply simp_all
     2.8 -   apply (erule prime_nd_one)
     2.9 -  apply (rule impI)
    2.10 -  apply (drule prime_dvd_mult)
    2.11 -   apply auto
    2.12 +   apply (force simp add: prime_def)
    2.13 +   apply (force dest: prime_dvd_mult)
    2.14    done
    2.15  
    2.16  lemma hd_xs_dvd_prod: