src/HOL/Library/Lattice_Syntax.thy
author nipkow
Tue, 07 Sep 2010 10:05:19 +0200
changeset 39198 f967a16dfcdd
parent 35787 afdf1c4958b2
child 41080 294956ff285b
permissions -rw-r--r--
expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
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
8291bc63d7c9 theory with syntax for lattice operations
haftmann
parents:
diff changeset
     5
theory Lattice_Syntax
32139
e271a64f03ff moved complete_lattice &c. into separate theory
haftmann
parents: 30375
diff changeset
     6
imports Complete_Lattice
30330
8291bc63d7c9 theory with syntax for lattice operations
haftmann
parents:
diff changeset
     7
begin
8291bc63d7c9 theory with syntax for lattice operations
haftmann
parents:
diff changeset
     8
8291bc63d7c9 theory with syntax for lattice operations
haftmann
parents:
diff changeset
     9
notation
32139
e271a64f03ff moved complete_lattice &c. into separate theory
haftmann
parents: 30375
diff changeset
    10
  top ("\<top>") and
e271a64f03ff moved complete_lattice &c. into separate theory
haftmann
parents: 30375
diff changeset
    11
  bot ("\<bottom>") and
30330
8291bc63d7c9 theory with syntax for lattice operations
haftmann
parents:
diff changeset
    12
  inf  (infixl "\<sqinter>" 70) and
8291bc63d7c9 theory with syntax for lattice operations
haftmann
parents:
diff changeset
    13
  sup  (infixl "\<squnion>" 65) and
8291bc63d7c9 theory with syntax for lattice operations
haftmann
parents:
diff changeset
    14
  Inf  ("\<Sqinter>_" [900] 900) and
32139
e271a64f03ff moved complete_lattice &c. into separate theory
haftmann
parents: 30375
diff changeset
    15
  Sup  ("\<Squnion>_" [900] 900)
30330
8291bc63d7c9 theory with syntax for lattice operations
haftmann
parents:
diff changeset
    16
30331
32ccef17d408 suppress document output
haftmann
parents: 30330
diff changeset
    17
end