Trim mapping definition
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Nicolas Méric 2022-04-20 16:27:53 +02:00
parent 3260ae3406
commit 30fc7a306f
1 changed files with 1 additions and 3 deletions

View File

@ -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>"