isabelle: src/HOL/Library/Lattice_Syntax.thy@8291bc63d7c9 (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
8291bc63d7c9 theory with syntax for lattice operations haftmann parents: diff changeset	5	theory Lattice_Syntax
8291bc63d7c9 theory with syntax for lattice operations haftmann parents: diff changeset	6	imports Set
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
8291bc63d7c9 theory with syntax for lattice operations haftmann parents: diff changeset	10	inf (infixl "\<sqinter>" 70) and
8291bc63d7c9 theory with syntax for lattice operations haftmann parents: diff changeset	11	sup (infixl "\<squnion>" 65) and
8291bc63d7c9 theory with syntax for lattice operations haftmann parents: diff changeset	12	Inf ("\<Sqinter>_" [900] 900) and
8291bc63d7c9 theory with syntax for lattice operations haftmann parents: diff changeset	13	Sup ("\<Squnion>_" [900] 900)
8291bc63d7c9 theory with syntax for lattice operations haftmann parents: diff changeset	14
8291bc63d7c9 theory with syntax for lattice operations haftmann parents: diff changeset	15	end

author	haftmann
	Fri, 06 Mar 2009 20:30:19 +0100
changeset 30330	8291bc63d7c9
child 30331	32ccef17d408
permissions	-rw-r--r--