equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Pocklington.thy |
1 (* Title: HOL/Library/Pocklington.thy |
2 ID: $Id$ |
|
3 Author: Amine Chaieb |
2 Author: Amine Chaieb |
4 *) |
3 *) |
5 |
4 |
6 header {* Pocklington's Theorem for Primes *} |
5 header {* Pocklington's Theorem for Primes *} |
7 |
6 |
8 |
|
9 theory Pocklington |
7 theory Pocklington |
10 imports Plain "~~/src/HOL/List" "~~/src/HOL/Primes" |
8 imports Main Primes |
11 begin |
9 begin |
12 |
10 |
13 definition modeq:: "nat => nat => nat => bool" ("(1[_ = _] '(mod _'))") |
11 definition modeq:: "nat => nat => nat => bool" ("(1[_ = _] '(mod _'))") |
14 where "[a = b] (mod p) == ((a mod p) = (b mod p))" |
12 where "[a = b] (mod p) == ((a mod p) = (b mod p))" |
15 |
13 |