isabelle: src/HOL/Library/Lattice_Syntax.thy@b8aeeedf7e68 (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
68660 4ce18f389f53 slightly more canonical imports haftmann parents: 66453 diff changeset	6	imports Main
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
68980 5717fbc55521 added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x nipkow parents: 68660 diff changeset	14	Inf ("\<Sqinter> _" [900] 900) and
5717fbc55521 added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x nipkow parents: 68660 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	wenzelm
	Tue, 05 Nov 2019 14:16:16 +0100
changeset 71046	b8aeeedf7e68
parent 68980	5717fbc55521
permissions	-rw-r--r--