summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/NumberTheory/ROOT.ML

author | paulson |

Thu Mar 20 15:58:25 2003 +0100 (2003-03-20) | |

changeset 13871 | 26e5f5e624f6 |

parent 11368 | 9c1995c73383 |

child 13887 | 54a0c675c423 |

permissions | -rw-r--r-- |

Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer

1 (* Title: HOL/NumberTheory/ROOT.ML

2 ID: $Id$

3 Author: Lawrence C Paulson

4 Copyright 2003 University of Cambridge

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

8 Kramer). The latter formalization follows Eisenstein's proof, which is the

9 one most commonly found in introductory textbooks, and also uses a

10 trick used David Russinoff with the Boyer-Moore theorem prover.

11 See his "A mechanical proof of quadratic reciprocity," Journal of Automated

12 Reasoning 8:3-21, 1992.

13 *)

15 no_document use_thy "Permutation";

16 no_document use_thy "Primes";

18 use_thy "Fib";

19 use_thy "Factorization";

20 use_thy "Chinese";

21 use_thy "EulerFermat";

22 use_thy "WilsonRuss";

23 use_thy "WilsonBij";

24 use_thy "Quadratic_Reciprocity";