equal
deleted
inserted
replaced
1361 |
1361 |
1362 \begin{itemize} |
1362 \begin{itemize} |
1363 |
1363 |
1364 \item Iterated replacement via recursive \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}. |
1364 \item Iterated replacement via recursive \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}. |
1365 For example, consider list enumeration \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{2C}{\isacharcomma}}\ c{\isaliteral{2C}{\isacharcomma}}\ d{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} as |
1365 For example, consider list enumeration \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{2C}{\isacharcomma}}\ c{\isaliteral{2C}{\isacharcomma}}\ d{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} as |
1366 defined in theory \hyperlink{theory.List}{\mbox{\isa{List}}} in Isabelle/HOL. |
1366 defined in theory \isa{List} in Isabelle/HOL. |
1367 |
1367 |
1368 \item Change of binding status of variables: anything beyond the |
1368 \item Change of binding status of variables: anything beyond the |
1369 built-in \hyperlink{keyword.binder}{\mbox{\isa{\isakeyword{binder}}}} mixfix annotation requires explicit |
1369 built-in \hyperlink{keyword.binder}{\mbox{\isa{\isakeyword{binder}}}} mixfix annotation requires explicit |
1370 syntax translations. For example, consider list filter |
1370 syntax translations. For example, consider list filter |
1371 comprehension \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}x\ {\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}\ xs\ {\isaliteral{2E}{\isachardot}}\ P{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} as defined in theory \hyperlink{theory.List}{\mbox{\isa{List}}} in Isabelle/HOL. |
1371 comprehension \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}x\ {\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}\ xs\ {\isaliteral{2E}{\isachardot}}\ P{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} as defined in theory \isa{List} in Isabelle/HOL. |
1372 |
1372 |
1373 \end{itemize}% |
1373 \end{itemize}% |
1374 \end{isamarkuptext}% |
1374 \end{isamarkuptext}% |
1375 \isamarkuptrue% |
1375 \isamarkuptrue% |
1376 % |
1376 % |