diff --git a/utp_pred.thy b/utp_pred.thy index e54fbb2..121de77 100644 --- a/utp_pred.thy +++ b/utp_pred.thy @@ -109,7 +109,7 @@ subsection \ Lattice syntax \ text \ In accordance with \cite{hoare1998}, we turn the lattice operators upside down \ -bundle utp_lattice_syntax +bundle UTP_lattice_syntax begin notation @@ -128,7 +128,25 @@ syntax end -unbundle utp_lattice_syntax +bundle no_UTP_lattice_syntax +begin + +no_notation + bot ("\") and + top ("\") and + inf (infixl "\" 70) and + sup (infixl "\" 65) and + Inf ("\ _" [900] 900) and + Sup ("\ _" [900] 900) + +no_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 + +unbundle UTP_lattice_syntax subsection \ Substitution Laws \