equal
deleted
inserted
replaced
2 ID: $Id$ 
2 ID: $Id$ 
3 Author: Lawrence C Paulson 
3 Author: Lawrence C Paulson 
4 Copyright 2003 University of Cambridge 
4 Copyright 2003 University of Cambridge 
5 
5 
6 This directory contains formalized proofs of Wilson's Theorem (by Thomas M 
6 This directory contains formalized proofs of Wilson's Theorem (by Thomas M 
7 Rasmussen) and of Gauss' law of quadratic reciprocity (by Avigad, Gray and 
7 Rasmussen) and of Gauss's law of quadratic reciprocity (by Avigad, Gray and 
8 Kramer). The latter formalization follows Eisenstein's proof, which is the 
8 Kramer). 
9 one most commonly found in introductory textbooks, and also uses a 
9 
10 trick used David Russinoff with the BoyerMoore theorem prover. 
10 The quadratic reciprocity formalization follows Eisenstein's proof, which is 
11 See his "A mechanical proof of quadratic reciprocity," Journal of Automated 
11 the one most commonly found in introductory textbooks, and also uses a trick 
12 Reasoning 8:321, 1992. 
12 used David Russinoff with the BoyerMoore theorem prover. See his "A 
13 *) 
13 mechanical proof of quadratic reciprocity," Journal of Automated Reasoning 

14 8:321, 1992.*) 
14 
15 
15 no_document use_thy "Permutation"; 
16 no_document use_thy "Permutation"; 
16 no_document use_thy "Primes"; 
17 no_document use_thy "Primes"; 
17 
18 
18 use_thy "Fib"; 
19 use_thy "Fib"; 