|
(* Author: Florian Haftmann, TU Muenchen *)
section \<open>Pretty syntax for lattice operations\<close>
theory Lattice_Syntax
imports Main
begin
notation
bot ("\") and
top ("\") and
inf (infixl "\" 70) and
sup (infixl "\" 65) and
Inf ("\ _" [900] 900) and
Sup ("\ _" [900] 900)
syntax
"_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10)
"_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)
"_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10)
"_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
