src/HOL/Library/Lattice_Syntax.thy
changeset 30331 32ccef17d408
parent 30330 8291bc63d7c9
child 30375 ad2a9dc516ed
     1.1 --- a/src/HOL/Library/Lattice_Syntax.thy	Fri Mar 06 20:30:19 2009 +0100
     1.2 +++ b/src/HOL/Library/Lattice_Syntax.thy	Sat Mar 07 10:06:12 2009 +0100
     1.3 @@ -2,6 +2,7 @@
     1.4  
     1.5  header {* Pretty syntax for lattice operations *}
     1.6  
     1.7 +(*<*)
     1.8  theory Lattice_Syntax
     1.9  imports Set
    1.10  begin
    1.11 @@ -12,4 +13,5 @@
    1.12    Inf  ("\<Sqinter>_" [900] 900) and
    1.13    Sup  ("\<Squnion>_" [900] 900)
    1.14  
    1.15 -end
    1.16 \ No newline at end of file
    1.17 +end
    1.18 +(*>*)
    1.19 \ No newline at end of file