376 The general idea of pretty printing with blocks and breaks is also |
376 The general idea of pretty printing with blocks and breaks is also |
377 described in \cite{paulson-ml2}.% |
377 described in \cite{paulson-ml2}.% |
378 \end{isamarkuptext}% |
378 \end{isamarkuptext}% |
379 \isamarkuptrue% |
379 \isamarkuptrue% |
380 % |
380 % |
381 \isamarkupsection{Explicit term notation% |
381 \isamarkupsection{Explicit notation% |
382 } |
382 } |
383 \isamarkuptrue% |
383 \isamarkuptrue% |
384 % |
384 % |
385 \begin{isamarkuptext}% |
385 \begin{isamarkuptext}% |
386 \begin{matharray}{rcll} |
386 \begin{matharray}{rcll} |
|
387 \indexdef{}{command}{type\_notation}\hypertarget{command.type-notation}{\hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
|
388 \indexdef{}{command}{no\_type\_notation}\hypertarget{command.no-type-notation}{\hyperlink{command.no-type-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}type{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
387 \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
389 \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
388 \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
390 \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
389 \end{matharray} |
391 \end{matharray} |
390 |
392 |
391 \begin{rail} |
393 \begin{rail} |
|
394 ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and') |
|
395 ; |
392 ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and') |
396 ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and') |
393 ; |
397 ; |
394 \end{rail} |
398 \end{rail} |
395 |
399 |
396 \begin{description} |
400 \begin{description} |
397 |
401 |
|
402 \item \hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix |
|
403 syntax with an existing type constructor. The arity of the |
|
404 constructor is retrieved from the context. |
|
405 |
|
406 \item \hyperlink{command.no-type-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}type{\isacharunderscore}notation}}}} is similar to \hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}, but removes the specified syntax annotation from |
|
407 the present context. |
|
408 |
398 \item \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix |
409 \item \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix |
399 syntax with an existing constant or fixed variable. This is a |
410 syntax with an existing constant or fixed variable. The type |
400 robust interface to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} primitive |
411 declaration of the given entity is retrieved from the context. |
401 (\secref{sec:syn-trans}). Type declaration and internal syntactic |
|
402 representation of the given entity is retrieved from the context. |
|
403 |
412 |
404 \item \hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, |
413 \item \hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, |
405 but removes the specified syntax annotation from the present |
414 but removes the specified syntax annotation from the present |
406 context. |
415 context. |
407 |
416 |
408 \end{description}% |
417 \end{description} |
|
418 |
|
419 Compared to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} and \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}} primitives (\secref{sec:syn-trans}), the above commands |
|
420 provide explicit checking wrt.\ the logical context, and work within |
|
421 general local theory targets, not just the global theory.% |
409 \end{isamarkuptext}% |
422 \end{isamarkuptext}% |
410 \isamarkuptrue% |
423 \isamarkuptrue% |
411 % |
424 % |
412 \isamarkupsection{The Pure syntax \label{sec:pure-syntax}% |
425 \isamarkupsection{The Pure syntax \label{sec:pure-syntax}% |
413 } |
426 } |