tuned header

--- a/src/HOL/Library/Determinants.thy	Mon Mar 23 08:14:22 2009 +0100
+++ b/src/HOL/Library/Determinants.thy	Mon Mar 23 08:14:23 2009 +0100
@@ -5,7 +5,7 @@
 header {* Traces, Determinant of square matrices and some properties *}
 
 theory Determinants
-  imports Euclidean_Space Permutations
+imports Euclidean_Space Permutations
 begin
 
 subsection{* First some facts about products*}

--- a/src/HOL/Library/Euclidean_Space.thy	Mon Mar 23 08:14:22 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy	Mon Mar 23 08:14:23 2009 +0100
@@ -5,10 +5,10 @@
 header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}
 
 theory Euclidean_Space
-  imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main
-  Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
-  Inner_Product
-  uses ("normarith.ML")
+imports
+  Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order" 
+  Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type Inner_Product
+uses ("normarith.ML")
 begin
 
 text{* Some common special cases.*}

--- a/src/HOL/Library/Finite_Cartesian_Product.thy	Mon Mar 23 08:14:22 2009 +0100
+++ b/src/HOL/Library/Finite_Cartesian_Product.thy	Mon Mar 23 08:14:23 2009 +0100
@@ -5,12 +5,9 @@
 header {* Definition of finite Cartesian product types. *}
 
 theory Finite_Cartesian_Product
-  (* imports Plain SetInterval ATP_Linkup *)
-imports Main
+imports Main (*FIXME: ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs.*)
 begin
 
-  (* FIXME : ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs*)
-
 definition hassize (infixr "hassize" 12) where
   "(S hassize n) = (finite S \<and> card S = n)"
 

--- a/src/HOL/Library/Formal_Power_Series.thy	Mon Mar 23 08:14:22 2009 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Mar 23 08:14:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      Formal_Power_Series.thy
-    ID:
     Author:     Amine Chaieb, University of Cambridge
 *)
 
 header{* A formalization of formal power series *}
 
 theory Formal_Power_Series
-  imports Main Fact Parity
+imports Main Fact Parity
 begin
 
 subsection {* The type of formal power series*}

--- a/src/HOL/Library/Glbs.thy	Mon Mar 23 08:14:22 2009 +0100
+++ b/src/HOL/Library/Glbs.thy	Mon Mar 23 08:14:23 2009 +0100
@@ -1,8 +1,6 @@
-(* Title:      Glbs
-   Author:     Amine Chaieb, University of Cambridge
-*)
+(* Author: Amine Chaieb, University of Cambridge *)
 
-header{*Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs*}
+header {* Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs *}
 
 theory Glbs
 imports Lubs

--- a/src/HOL/Library/Order_Relation.thy	Mon Mar 23 08:14:22 2009 +0100
+++ b/src/HOL/Library/Order_Relation.thy	Mon Mar 23 08:14:23 2009 +0100
@@ -1,6 +1,4 @@
-(*  ID          : $Id$
-    Author      : Tobias Nipkow
-*)
+(* Author: Tobias Nipkow *)
 
 header {* Orders as Relations *}
 

--- a/src/HOL/ex/MergeSort.thy	Mon Mar 23 08:14:22 2009 +0100
+++ b/src/HOL/ex/MergeSort.thy	Mon Mar 23 08:14:23 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ex/Merge.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   2002 TU Muenchen
 *)