diff -r 9d8cd1ca8c61 -r afdf1c4958b2 src/HOL/Library/Quotient_Syntax.thy
--- a/src/HOL/Library/Quotient_Syntax.thy	Sun Mar 14 14:10:21 2010 +0100
+++ b/src/HOL/Library/Quotient_Syntax.thy	Sun Mar 14 14:29:30 2010 +0100
@@ -1,10 +1,9 @@
-(*  Title:      Quotient_Syntax.thy
+(*  Title:      HOL/Library/Quotient_Syntax.thy
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
 header {* Pretty syntax for Quotient operations *}
 
-(*<*)
 theory Quotient_Syntax
 imports Main
 begin
@@ -15,4 +14,3 @@
   fun_rel (infixr "===>" 55)
 
 end
-(*>*)