src/HOL/Library/Quotient_Syntax.thy
changeset 35787 afdf1c4958b2
parent 35222 4f1fba00f66d
child 40602 91e583511113
     1.1 --- a/src/HOL/Library/Quotient_Syntax.thy	Sun Mar 14 14:10:21 2010 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Syntax.thy	Sun Mar 14 14:29:30 2010 +0100
     1.3 @@ -1,10 +1,9 @@
     1.4 -(*  Title:      Quotient_Syntax.thy
     1.5 +(*  Title:      HOL/Library/Quotient_Syntax.thy
     1.6      Author:     Cezary Kaliszyk and Christian Urban
     1.7  *)
     1.8  
     1.9  header {* Pretty syntax for Quotient operations *}
    1.10  
    1.11 -(*<*)
    1.12  theory Quotient_Syntax
    1.13  imports Main
    1.14  begin
    1.15 @@ -15,4 +14,3 @@
    1.16    fun_rel (infixr "===>" 55)
    1.17  
    1.18  end
    1.19 -(*>*)