changeset 21404 | eb85850d3eb7 |
parent 19670 | 2e4a143c73c5 |
child 23814 | cdaa6b701509 |
--- a/src/HOL/NumberTheory/Factorization.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/NumberTheory/Factorization.thy Fri Nov 17 02:20:03 2006 +0100 @@ -12,7 +12,7 @@ subsection {* Definitions *} definition - primel :: "nat list => bool " + primel :: "nat list => bool" where "primel xs = (\<forall>p \<in> set xs. prime p)" consts