equal
deleted
inserted
replaced
185 \end{isabelle} |
185 \end{isabelle} |
186 |
186 |
187 The simplest morphism is the @{ML_ind identity in Morphism}-morphism defined as |
187 The simplest morphism is the @{ML_ind identity in Morphism}-morphism defined as |
188 *} |
188 *} |
189 |
189 |
190 ML{*val identity = Morphism.morphism {binding = I, typ = I, term = I, fact = I}*} |
190 ML{*val identity = Morphism.morphism {binding = [], typ = [], term = [], fact = []}*} |
191 |
191 |
192 text {* |
192 text {* |
193 Morphisms can be composed with the function @{ML_ind "$>" in Morphism} |
193 Morphisms can be composed with the function @{ML_ind "$>" in Morphism} |
194 *} |
194 *} |
195 |
195 |