src/HOL/Library/Quotient_Syntax.thy
changeset 35787 afdf1c4958b2
parent 35222 4f1fba00f66d
child 40602 91e583511113
--- 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
-(*>*)