--- 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
--- 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
-(*>*)