isabelle: src/HOL/Library/Lattice_Syntax.thy@6a85b8a9c28c (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
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 61955 diff changeset	6	imports HOL.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	haftmann
	Thu, 16 Nov 2017 11:30:23 +0100
changeset 67078	6a85b8a9c28c
parent 66453	cc19f7ca2ed6
child 68660	4ce18f389f53
permissions	-rw-r--r--