src/HOL/Old_Number_Theory/Finite2.thy
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{*