equal
deleted
inserted
replaced
39 % |
39 % |
40 \begin{isamarkuptext}% |
40 \begin{isamarkuptext}% |
41 When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command it is possible to leave |
41 When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command it is possible to leave |
42 out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} part; then code is distributed over |
42 out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} part; then code is distributed over |
43 different modules, where the module name space roughly is induced |
43 different modules, where the module name space roughly is induced |
44 by the \isa{Isabelle} theory namespace. |
44 by the \isa{Isabelle} theory name space. |
45 |
45 |
46 Then sometimes the awkward situation occurs that dependencies between |
46 Then sometimes the awkward situation occurs that dependencies between |
47 definitions introduce cyclic dependencies between modules, which in the |
47 definitions introduce cyclic dependencies between modules, which in the |
48 \isa{Haskell} world leaves you to the mercy of the \isa{Haskell} implementation |
48 \isa{Haskell} world leaves you to the mercy of the \isa{Haskell} implementation |
49 you are using, while for \isa{SML}/\isa{OCaml} code generation is not possible. |
49 you are using, while for \isa{SML}/\isa{OCaml} code generation is not possible. |