isabelle: src/HOL/Library/Lattice_Syntax.thy@e96383acecf9 (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
44860 56101fa00193 renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc. haftmann parents: 41082 diff changeset	6	imports Complete_Lattices
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
41082 9ff94e7cc3b3 bot comes before top, inf before sup etc. haftmann parents: 41080 diff changeset	10	bot ("\<bottom>") and
32139 e271a64f03ff moved complete_lattice &c. into separate theory haftmann parents: 30375 diff changeset	11	top ("\<top>") 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
41080 294956ff285b nice syntax for lattice INFI, SUPR; haftmann parents: 35787 diff changeset	17	syntax (xsymbols)
41082 9ff94e7cc3b3 bot comes before top, inf before sup etc. haftmann parents: 41080 diff changeset	18	"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
9ff94e7cc3b3 bot comes before top, inf before sup etc. haftmann parents: 41080 diff changeset	19	"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
41080 294956ff285b nice syntax for lattice INFI, SUPR; haftmann parents: 35787 diff changeset	20	"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
294956ff285b nice syntax for lattice INFI, SUPR; haftmann parents: 35787 diff changeset	21	"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
294956ff285b nice syntax for lattice INFI, SUPR; haftmann parents: 35787 diff changeset	22
30331 32ccef17d408 suppress document output haftmann parents: 30330 diff changeset	23	end

author	blanchet
	Thu, 06 Mar 2014 15:40:33 +0100
changeset 55945	e96383acecf9
parent 44860	56101fa00193
child 58881	b9556a055632
permissions	-rw-r--r--