1 (*<*)

     1 (*<*)

     2 theory Paper

     2 theory Paper

     3 imports "Quotient"

     3 imports "Quotient"

     4         "LaTeXsugar"

     4         "LaTeXsugar"

     5 begin

     6 begin

     6 

     7 

     7 notation (latex output)

     8 notation (latex output)

     8   rel_conj ("_ OOO _" [53, 53] 52)

     9   rel_conj ("_ OOO _" [53, 53] 52)

     9 and

    10 and