diff --git a/src/HOL/Library/Library.thy b/src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy
+++ b/src/HOL/Library/Library.thy
@@ -1,106 +1,106 @@
-  (*<*)
+(*<*)
 theory Library
 imports
   AList
   Adhoc_Overloading
   BigO
   Bit_Operations
   BNF_Axiomatization
   BNF_Corec
   Boolean_Algebra
   Bourbaki_Witt_Fixpoint
   Char_ord
   Code_Lazy
   Code_Test
   Combine_PER
   Complete_Partial_Order2
   Conditional_Parametricity
   Confluence
   Confluent_Quotient
   Countable
   Countable_Complete_Lattices
   Countable_Set_Type
   Debug
   Diagonal_Subsequence
   Discrete
   Disjoint_Sets
   Dlist
   Dual_Ordered_Lattice
   Equipollence
   Extended
   Extended_Nat
   Extended_Nonnegative_Real
   Extended_Real
   Finite_Map
   Float
   FSet
   FuncSet
   Function_Division
   Fun_Lexorder
   Going_To_Filter
   Groups_Big_Fun
   Indicator_Function
   Infinite_Set
   Interval
   Interval_Float
   IArray
   Landau_Symbols
   Lattice_Algebras
   Lattice_Syntax
   Lattice_Constructions
   Linear_Temporal_Logic_on_Streams
   ListVector
   Lub_Glb
   Mapping
   Monad_Syntax
   More_List
   Multiset_Order
   Multiset_Permutations
   Nonpos_Ints
   Numeral_Type
   Omega_Words_Fun
   Open_State_Syntax
   Option_ord
   Order_Continuity
   Parallel
   Pattern_Aliases
   Periodic_Fun
   Perm
   Permutation
   Permutations
   Poly_Mapping
   Power_By_Squaring
   Preorder
   Product_Plus
   Quadratic_Discriminant
   Quotient_List
   Quotient_Option
   Quotient_Product
   Quotient_Set
   Quotient_Sum
   Quotient_Syntax
   Quotient_Type
   Ramsey
   Reflection
   Rewrite
   Saturated
   Set_Algebras
   Set_Idioms
   Signed_Division
   State_Monad
   Stirling
   Stream
   Sorting_Algorithms
   Sublist
   Sum_of_Squares
   Transitive_Closure_Table
   Tree_Multiset
   Tree_Real
   Type_Length
   Uprod
   While_Combinator
   Word
   Z2
 begin
 end
 (*>*)