Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplified a proof using new dvd rules
authorpaulson
Sat, 09 Jun 2001 08:42:06 +0200
changeset 11364 01020b10c0a7
parent 11363 a548865b1b6a
child 11365 6d5698df0413
simplified a proof using new dvd rules
src/HOL/IMPP/EvenOdd.ML file | annotate | diff | comparison | revisions
src/HOL/NumberTheory/Factorization.thy file | annotate | diff | comparison | revisions 
--- 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];
 
--- 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:
isabelle