src/HOL/Library/Lattice_Syntax.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 32139 e271a64f03ff
child 35787 afdf1c4958b2
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
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@32139
     7
imports Complete_Lattice
haftmann@30330
     8
begin
haftmann@30330
     9
haftmann@30330
    10
notation
haftmann@32139
    11
  top ("\<top>") and
haftmann@32139
    12
  bot ("\<bottom>") and
haftmann@30330
    13
  inf  (infixl "\<sqinter>" 70) and
haftmann@30330
    14
  sup  (infixl "\<squnion>" 65) and
haftmann@30330
    15
  Inf  ("\<Sqinter>_" [900] 900) and
haftmann@32139
    16
  Sup  ("\<Squnion>_" [900] 900)
haftmann@30330
    17
haftmann@30331
    18
end
haftmann@30331
    19
(*>*)