Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Lattice_Syntax.thy
author himmelma
Thu, 28 May 2009 18:59:51 +0200
changeset 31283 86093a969bcd
parent 30375 ad2a9dc516ed
child 32139 e271a64f03ff
permissions -rw-r--r--
Removed Convex_Euclidean_Space.thy from Library.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30330
8291bc63d7c9 theory with syntax for lattice operations
haftmann
parents:
diff changeset 
     1
 
(* Author: Florian Haftmann, TU Muenchen *)
8291bc63d7c9 theory with syntax for lattice operations
haftmann
parents:
diff changeset 
     2
 












8291bc63d7c9
theory with syntax for lattice operations



haftmann


parents: 

diff
changeset




     3


header {* Pretty syntax for lattice operations *}













8291bc63d7c9
theory with syntax for lattice operations



haftmann


parents: 

diff
changeset




     4









30331






32ccef17d408
suppress document output



haftmann


parents: 
30330

diff
changeset




     5


(*<*)








30330






8291bc63d7c9
theory with syntax for lattice operations



haftmann


parents: 

diff
changeset




     6


theory Lattice_Syntax













8291bc63d7c9
theory with syntax for lattice operations



haftmann


parents: 

diff
changeset




     7


imports Set













8291bc63d7c9
theory with syntax for lattice operations



haftmann


parents: 

diff
changeset




     8


begin













8291bc63d7c9
theory with syntax for lattice operations



haftmann


parents: 

diff
changeset




     9














8291bc63d7c9
theory with syntax for lattice operations



haftmann


parents: 

diff
changeset




    10


notation













8291bc63d7c9
theory with syntax for lattice operations



haftmann


parents: 

diff
changeset




    11


  inf  (infixl "\<sqinter>" 70) and













8291bc63d7c9
theory with syntax for lattice operations



haftmann


parents: 

diff
changeset




    12


  sup  (infixl "\<squnion>" 65) and













8291bc63d7c9
theory with syntax for lattice operations



haftmann


parents: 

diff
changeset




    13


  Inf  ("\<Sqinter>_" [900] 900) and








30375






ad2a9dc516ed
added top and bot syntax



haftmann


parents: 
30331

diff
changeset




    14


  Sup  ("\<Squnion>_" [900] 900) and













ad2a9dc516ed
added top and bot syntax



haftmann


parents: 
30331

diff
changeset




    15


  top ("\<top>") and













ad2a9dc516ed
added top and bot syntax



haftmann


parents: 
30331

diff
changeset




    16


  bot ("\<bottom>")








30330






8291bc63d7c9
theory with syntax for lattice operations



haftmann


parents: 

diff
changeset




    17









30331






32ccef17d408
suppress document output



haftmann


parents: 
30330

diff
changeset




    18


end













32ccef17d408
suppress document output



haftmann


parents: 
30330

diff
changeset




    19


(*>*)














isabelle