suppress document output
authorhaftmann
Sat, 07 Mar 2009 10:06:12 +0100
changeset 30331 32ccef17d408
parent 30330 8291bc63d7c9
child 30332 0d07f4823d3a
suppress document output
src/HOL/Library/Lattice_Syntax.thy
--- a/src/HOL/Library/Lattice_Syntax.thy	Fri Mar 06 20:30:19 2009 +0100
+++ b/src/HOL/Library/Lattice_Syntax.thy	Sat Mar 07 10:06:12 2009 +0100
@@ -2,6 +2,7 @@
 
 header {* Pretty syntax for lattice operations *}
 
+(*<*)
 theory Lattice_Syntax
 imports Set
 begin
@@ -12,4 +13,5 @@
   Inf  ("\<Sqinter>_" [900] 900) and
   Sup  ("\<Squnion>_" [900] 900)
 
-end
\ No newline at end of file
+end
+(*>*)
\ No newline at end of file