# HG changeset patch
# User haftmann
# Date 1236416772 -3600
# Node ID 32ccef17d4080f4b19be53b097955bc96025e269
# Parent  8291bc63d7c912f1b797ed518d0988633056fbd5
suppress document output

diff -r 8291bc63d7c9 -r 32ccef17d408 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