From 298acc4b5e11c4628dd762996243b6d30f1563d4 Mon Sep 17 00:00:00 2001
From: Simon Foster <simon.foster@york.ac.uk>
Date: Tue, 30 Jan 2024 14:35:50 +0000
Subject: [PATCH] Fixed broken proof

---
 utp_des_laws.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/utp_des_laws.thy b/utp_des_laws.thy
index 74c9e5b..0df503c 100644
--- a/utp_des_laws.thy
+++ b/utp_des_laws.thy
@@ -428,6 +428,6 @@ lemma design_bottom:
 lemma design_refine_thms:
   assumes "P \<sqsubseteq> Q"
   shows "`pre\<^sub>D(P) \<longrightarrow> pre\<^sub>D(Q)`" "`pre\<^sub>D(P) \<and> post\<^sub>D(Q) \<longrightarrow> post\<^sub>D(P)`"
-  using assms unfolding pred_refine_iff by (pred_auto, blast, pred_auto)
+  using assms unfolding pred_refine_iff by (pred_auto, blast, pred_auto, blast)
 
 end
\ No newline at end of file