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

src/HOL/NumberTheory/ROOT.ML

author | paulson |

Fri Mar 05 11:43:55 2004 +0100 (2004-03-05) | |

changeset 14434 | 5f14c1207499 |

parent 14271 | 8ed6989228bb |

child 19671 | e293e16d1442 |

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

patch to NumberTheory problems caused by Parity

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's law of quadratic reciprocity (by Avigad, Gray and

8 Kramer).

10 The quadratic reciprocity formalization follows Eisenstein's proof, which is

11 the one most commonly found in introductory textbooks, and also uses a trick

12 used David Russinoff with the Boyer-Moore theorem prover. See his "A

13 mechanical proof of quadratic reciprocity," Journal of Automated Reasoning

14 8:3-21, 1992.*)

16 no_document use_thy "Permutation";

17 no_document use_thy "Primes";

19 use_thy "Fib";

20 use_thy "Factorization";

21 use_thy "Chinese";

22 use_thy "WilsonRuss";

23 use_thy "WilsonBij";

24 use_thy "Quadratic_Reciprocity";