From 9d4779dbefd48df8e4a3ab066836030610b0447a Mon Sep 17 00:00:00 2001
From: rye <ye.randall@gmail.com>
Date: Fri, 2 Sep 2022 23:17:35 +0100
Subject: [PATCH] Add a bundle no_UTP_lattice_syntax to switch off UTP lattice
 syntax

---
 utp_pred.thy | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

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 \<open> Lattice syntax \<close>
 
 text \<open> In accordance with \cite{hoare1998}, we turn the lattice operators upside down \<close>
 
-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 ("\<top>") and
+  top ("\<bottom>") and
+  inf  (infixl "\<squnion>" 70) and
+  sup  (infixl "\<sqinter>" 65) and
+  Inf  ("\<Squnion> _" [900] 900) and
+  Sup  ("\<Sqinter> _" [900] 900)
+
+no_syntax
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+end
+
+unbundle UTP_lattice_syntax
 
 subsection \<open> Substitution Laws \<close>