equal
deleted
inserted
replaced
5 |
5 |
6 header {* Pocklington's Theorem for Primes *} |
6 header {* Pocklington's Theorem for Primes *} |
7 |
7 |
8 |
8 |
9 theory Pocklington |
9 theory Pocklington |
10 imports Plain List Primes |
10 imports Plain "~~/src/HOL/List" "~~/src/HOL/Primes" |
11 begin |
11 begin |
12 |
12 |
13 definition modeq:: "nat => nat => nat => bool" ("(1[_ = _] '(mod _'))") |
13 definition modeq:: "nat => nat => nat => bool" ("(1[_ = _] '(mod _'))") |
14 where "[a = b] (mod p) == ((a mod p) = (b mod p))" |
14 where "[a = b] (mod p) == ((a mod p) = (b mod p))" |
15 |
15 |