# HG changeset patch
# User wenzelm
# Date 1268573370 -3600
# Node ID afdf1c4958b2b189a0f520bf896eda5b3cf748e9
# Parent  9d8cd1ca8c6144610ca6fb8ef2395a0c1edc4bdc
expose formal text;

diff -r 9d8cd1ca8c61 -r afdf1c4958b2 src/HOL/Library/Lattice_Syntax.thy
--- a/src/HOL/Library/Lattice_Syntax.thy	Sun Mar 14 14:10:21 2010 +0100
+++ b/src/HOL/Library/Lattice_Syntax.thy	Sun Mar 14 14:29:30 2010 +0100
@@ -2,7 +2,6 @@
 
 header {* Pretty syntax for lattice operations *}
 
-(*<*)
 theory Lattice_Syntax
 imports Complete_Lattice
 begin
@@ -16,4 +15,3 @@
   Sup  ("\<Squnion>_" [900] 900)
 
 end
-(*>*)
\ No newline at end of file
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
-(*>*)