Fixed broken proof

isabelle-utp · Jan 30, 2024 · 298acc4 · 298acc4
1 parent 8c7e4d2
commit 298acc4
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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