isabelle: src/HOL/Library/Lattice_Syntax.thy@98809b3f5e3c (annotated)

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	(>)

author	nipkow
	Wed, 01 Apr 2009 18:41:15 +0200
changeset 30840	98809b3f5e3c
parent 30375	ad2a9dc516ed
child 32139	e271a64f03ff
permissions	-rw-r--r--