src/HOL/Library/Quotient_Option.thy

--- a/src/HOL/Library/Quotient_Option.thy	Sun Mar 14 14:29:30 2010 +0100
+++ b/src/HOL/Library/Quotient_Option.thy	Sun Mar 14 14:31:24 2010 +0100
@@ -1,12 +1,13 @@
-(*  Title:      Quotient_Option.thy
+(*  Title:      HOL/Library/Quotient_Option.thy
     Author:     Cezary Kaliszyk and Christian Urban
 *)
+
+header {* Quotient infrastructure for the option type *}
+
 theory Quotient_Option
 imports Main Quotient_Syntax
 begin
 
-section {* Quotient infrastructure for the option type. *}
-
 fun
   option_rel
 where