src/HOL/Old_Number_Theory/Finite2.thy
changeset 38159 e9b4835a54ee
parent 32479 521cc9bf2958
child 40786 0a54cfc9add3
     1.1 --- a/src/HOL/Old_Number_Theory/Finite2.thy	Thu Aug 05 23:43:43 2010 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/Finite2.thy	Fri Aug 06 12:37:00 2010 +0200
     1.3 @@ -1,12 +1,11 @@
     1.4 -(*  Title:      HOL/Quadratic_Reciprocity/Finite2.thy
     1.5 -    ID:         $Id$
     1.6 +(*  Title:      HOL/Old_Number_Theory/Finite2.thy
     1.7      Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     1.8  *)
     1.9  
    1.10  header {*Finite Sets and Finite Sums*}
    1.11  
    1.12  theory Finite2
    1.13 -imports Main IntFact Infinite_Set
    1.14 +imports IntFact Infinite_Set
    1.15  begin
    1.16  
    1.17  text{*