| changeset 21404 | eb85850d3eb7 |
| parent 19670 | 2e4a143c73c5 |
| child 23814 | cdaa6b701509 |
| 21403:dd58f13a8eb4 | 21404:eb85850d3eb7 |
|---|---|
10 |
10 |
11 |
11 |
12 subsection {* Definitions *} |
12 subsection {* Definitions *} |
13 |
13 |
14 definition |
14 definition |
15 primel :: "nat list => bool " |
15 primel :: "nat list => bool" where |
16 "primel xs = (\<forall>p \<in> set xs. prime p)" |
16 "primel xs = (\<forall>p \<in> set xs. prime p)" |
17 |
17 |
18 consts |
18 consts |
19 nondec :: "nat list => bool " |
19 nondec :: "nat list => bool " |
20 prod :: "nat list => nat" |
20 prod :: "nat list => nat" |