author | paulson |

Mon Mar 31 12:29:26 2003 +0200 (2003-03-31) | |

changeset 13887 | 54a0c675c423 |

parent 13886 | 0b243f6e257e |

child 13888 | 16f424af58a2 |

tidied

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