isabelle: src/HOL/Library/Lattice_Syntax.thy@1bc6816fd525 (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
60500 903bb1495239 isabelle update_cartouches; wenzelm parents: 58881 diff changeset	3	section \<open>Pretty syntax for lattice operations\<close>
30330 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
61955 e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; wenzelm parents: 60500 diff changeset	17	syntax
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	Andreas Lochbihler
	Tue, 07 Jun 2016 15:12:27 +0200
changeset 63243	1bc6816fd525
parent 61955	e96292f32c3c
child 66453	cc19f7ca2ed6
permissions	-rw-r--r--