summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Mon, 31 Mar 2003 12:29:26 +0200 | |

changeset 13887 | 54a0c675c423 |

parent 13886 | 0b243f6e257e |

child 13888 | 16f424af58a2 |

tidied

--- a/src/HOL/NumberTheory/ROOT.ML Sat Mar 29 12:28:53 2003 +0100 +++ b/src/HOL/NumberTheory/ROOT.ML Mon Mar 31 12:29:26 2003 +0200 @@ -4,13 +4,14 @@ Copyright 2003 University of Cambridge This directory contains formalized proofs of Wilson's Theorem (by Thomas M -Rasmussen) and of Gauss' law of quadratic reciprocity (by Avigad, Gray and -Kramer). The latter formalization follows Eisenstein's proof, which is the -one most commonly found in introductory textbooks, and also uses a -trick used David Russinoff with the Boyer-Moore theorem prover. -See his "A mechanical proof of quadratic reciprocity," Journal of Automated -Reasoning 8:3-21, 1992. -*) +Rasmussen) and of Gauss's law of quadratic reciprocity (by Avigad, Gray and +Kramer). + +The quadratic reciprocity formalization follows Eisenstein's proof, which is +the one most commonly found in introductory textbooks, and also uses a trick +used David Russinoff with the Boyer-Moore theorem prover. See his "A +mechanical proof of quadratic reciprocity," Journal of Automated Reasoning +8:3-21, 1992.*) no_document use_thy "Permutation"; no_document use_thy "Primes";