From 30fc7a306fba8bc2ebb165d15a2a35363dfb4fdb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Wed, 20 Apr 2022 16:27:53 +0200
Subject: [PATCH] Trim mapping definition

---
 examples/scholarly_paper/2021-ITP-PMTI/paper.thy | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
index bca4411..80544ff 100644
--- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
+++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
@@ -929,9 +929,7 @@ equals the sum of all the masses of the products composing the object.
 text\<open>
 \begin{figure}
 @{boxed_theory_text [display]
-\<open>
-
-definition Item_to_Resource_morphism :: "Item \<Rightarrow> Resource" 
+\<open>definition Item_to_Resource_morphism :: "Item \<Rightarrow> Resource" 
            ("_ \<langle>Resource\<rangle>\<^sub>I\<^sub>t\<^sub>e\<^sub>m" [1000]999)
   where    "\<sigma> \<langle>Resource\<rangle>\<^sub>I\<^sub>t\<^sub>e\<^sub>m =  \<lparr>  Resource.tag_attribute = 0::int , 
                                  Resource.name = name \<sigma> \<rparr>"