summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/NumberTheory/ROOT.ML

author | paulson |

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

changeset 13887 | 54a0c675c423 |

parent 13871 | 26e5f5e624f6 |

child 14271 | 8ed6989228bb |

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

tidied

(* 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.*) no_document use_thy "Permutation"; no_document use_thy "Primes"; use_thy "Fib"; use_thy "Factorization"; use_thy "Chinese"; use_thy "EulerFermat"; use_thy "WilsonRuss"; use_thy "WilsonBij"; use_thy "Quadratic_Reciprocity";