isabelle: src/HOL/Library/Lattice_Syntax.thy@97775f3e8722 (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
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

author	haftmann
	Fri, 27 Aug 2010 19:34:23 +0200
changeset 38857	97775f3e8722
parent 35787	afdf1c4958b2
child 41080	294956ff285b
permissions	-rw-r--r--