From cb2b0dc23052c5d26c07489076ab534102cee408 Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolff@lri.fr>
Date: Thu, 6 Apr 2023 15:23:55 +0200
Subject: [PATCH] ...

---
 Isabelle_DOF-Example-II/paper.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Isabelle_DOF-Example-II/paper.thy b/Isabelle_DOF-Example-II/paper.thy
index 44f04e1f..1f7f9cfc 100644
--- a/Isabelle_DOF-Example-II/paper.thy
+++ b/Isabelle_DOF-Example-II/paper.thy
@@ -573,7 +573,7 @@ be deadlocked after any non-terminating trace.
 \<close>
 
 Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>", level="Some 2"]
-\<open> \<^hfill> \<^break> \<open>deadlock_free P \<longleftrightarrow> (\<forall>s\<in>\<T> P. tickFree s \<longrightarrow> (s, {\<surd>}\<union>events_of P) \<notin> \<F> P)\<close> \<close>   
+\<open> \<^hfill> \<^br> \<open>deadlock_free P \<longleftrightarrow> (\<forall>s\<in>\<T> P. tickFree s \<longrightarrow> (s, {\<surd>}\<union>events_of P) \<notin> \<F> P)\<close> \<close>   
 Definition*[X11, level="Some 2"]\<open>  \<open>livelock\<^sub>-free P \<equiv> \<D> P = {} \<close>   \<close>
 
 text\<open> Recall that all five reference processes are livelock-free.