changeset 38159 | e9b4835a54ee |
parent 32479 | 521cc9bf2958 |
child 40786 | 0a54cfc9add3 |
--- a/src/HOL/Old_Number_Theory/Finite2.thy Thu Aug 05 23:43:43 2010 +0200 +++ b/src/HOL/Old_Number_Theory/Finite2.thy Fri Aug 06 12:37:00 2010 +0200 @@ -1,12 +1,11 @@ -(* Title: HOL/Quadratic_Reciprocity/Finite2.thy - ID: $Id$ +(* Title: HOL/Old_Number_Theory/Finite2.thy Authors: Jeremy Avigad, David Gray, and Adam Kramer *) header {*Finite Sets and Finite Sums*} theory Finite2 -imports Main IntFact Infinite_Set +imports IntFact Infinite_Set begin text{*