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

author | wenzelm |

Wed, 17 May 2006 01:23:43 +0200 | |

changeset 19671 | e293e16d1442 |

parent 19670 | 2e4a143c73c5 |

child 19672 | 9be07d531694 |

removed outdated/redundant comments;

--- a/src/HOL/NumberTheory/ROOT.ML Wed May 17 01:23:41 2006 +0200 +++ b/src/HOL/NumberTheory/ROOT.ML Wed May 17 01:23:43 2006 +0200 @@ -1,17 +1,4 @@ -(* Title: HOL/NumberTheory/ROOT.ML - ID: $Id$ - Author: Lawrence C Paulson - Copyright 2003 University of Cambridge - -This directory contains formalized proofs of Wilson's Theorem (by Thomas M -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.*) +(* $Id$ *) no_document use_thy "Permutation"; no_document use_thy "Primes";