src/HOL/Library/Lattice_Syntax.thy
author haftmann
Sat Mar 07 10:06:12 2009 +0100 (2009-03-07)
changeset 30331 32ccef17d408
parent 30330 8291bc63d7c9
child 30375 ad2a9dc516ed
permissions -rw-r--r--
suppress document output
haftmann@30330
     1
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@30330
     2
haftmann@30330
     3
header {* Pretty syntax for lattice operations *}
haftmann@30330
     4
haftmann@30331
     5
(*<*)
haftmann@30330
     6
theory Lattice_Syntax
haftmann@30330
     7
imports Set
haftmann@30330
     8
begin
haftmann@30330
     9
haftmann@30330
    10
notation
haftmann@30330
    11
  inf  (infixl "\<sqinter>" 70) and
haftmann@30330
    12
  sup  (infixl "\<squnion>" 65) and
haftmann@30330
    13
  Inf  ("\<Sqinter>_" [900] 900) and
haftmann@30330
    14
  Sup  ("\<Squnion>_" [900] 900)
haftmann@30330
    15
haftmann@30331
    16
end
haftmann@30331
    17
(*>*)