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