91 The Isabelle/Isar outer syntax provides token classes as presented |
91 The Isabelle/Isar outer syntax provides token classes as presented |
92 below; most of these coincide with the inner lexical syntax as |
92 below; most of these coincide with the inner lexical syntax as |
93 presented in \cite{isabelle-ref}. |
93 presented in \cite{isabelle-ref}. |
94 |
94 |
95 \begin{matharray}{rcl} |
95 \begin{matharray}{rcl} |
96 \indexdef{}{syntax}{ident}\mbox{\isa{ident}} & = & letter\,quasiletter^* \\ |
96 \indexdef{}{syntax}{ident}\hypertarget{syntax.ident}{\hyperlink{syntax.ident}{\mbox{\isa{ident}}}} & = & letter\,quasiletter^* \\ |
97 \indexdef{}{syntax}{longident}\mbox{\isa{longident}} & = & ident (\verb,.,ident)^+ \\ |
97 \indexdef{}{syntax}{longident}\hypertarget{syntax.longident}{\hyperlink{syntax.longident}{\mbox{\isa{longident}}}} & = & ident (\verb,.,ident)^+ \\ |
98 \indexdef{}{syntax}{symident}\mbox{\isa{symident}} & = & sym^+ ~|~ \verb,\,\verb,<,ident\verb,>, \\ |
98 \indexdef{}{syntax}{symident}\hypertarget{syntax.symident}{\hyperlink{syntax.symident}{\mbox{\isa{symident}}}} & = & sym^+ ~|~ \verb,\,\verb,<,ident\verb,>, \\ |
99 \indexdef{}{syntax}{nat}\mbox{\isa{nat}} & = & digit^+ \\ |
99 \indexdef{}{syntax}{nat}\hypertarget{syntax.nat}{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}} & = & digit^+ \\ |
100 \indexdef{}{syntax}{var}\mbox{\isa{var}} & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\ |
100 \indexdef{}{syntax}{var}\hypertarget{syntax.var}{\hyperlink{syntax.var}{\mbox{\isa{var}}}} & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\ |
101 \indexdef{}{syntax}{typefree}\mbox{\isa{typefree}} & = & \verb,',ident \\ |
101 \indexdef{}{syntax}{typefree}\hypertarget{syntax.typefree}{\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}}} & = & \verb,',ident \\ |
102 \indexdef{}{syntax}{typevar}\mbox{\isa{typevar}} & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\ |
102 \indexdef{}{syntax}{typevar}\hypertarget{syntax.typevar}{\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}}} & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\ |
103 \indexdef{}{syntax}{string}\mbox{\isa{string}} & = & \verb,", ~\dots~ \verb,", \\ |
103 \indexdef{}{syntax}{string}\hypertarget{syntax.string}{\hyperlink{syntax.string}{\mbox{\isa{string}}}} & = & \verb,", ~\dots~ \verb,", \\ |
104 \indexdef{}{syntax}{altstring}\mbox{\isa{altstring}} & = & \backquote ~\dots~ \backquote \\ |
104 \indexdef{}{syntax}{altstring}\hypertarget{syntax.altstring}{\hyperlink{syntax.altstring}{\mbox{\isa{altstring}}}} & = & \backquote ~\dots~ \backquote \\ |
105 \indexdef{}{syntax}{verbatim}\mbox{\isa{verbatim}} & = & \verb,{*, ~\dots~ \verb,*,\verb,}, \\[1ex] |
105 \indexdef{}{syntax}{verbatim}\hypertarget{syntax.verbatim}{\hyperlink{syntax.verbatim}{\mbox{\isa{verbatim}}}} & = & \verb,{*, ~\dots~ \verb,*,\verb,}, \\[1ex] |
106 |
106 |
107 letter & = & latin ~|~ \verb,\,\verb,<,latin\verb,>, ~|~ \verb,\,\verb,<,latin\,latin\verb,>, ~|~ greek ~|~ \\ |
107 letter & = & latin ~|~ \verb,\,\verb,<,latin\verb,>, ~|~ \verb,\,\verb,<,latin\,latin\verb,>, ~|~ greek ~|~ \\ |
108 & & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\ |
108 & & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\ |
109 quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\ |
109 quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\ |
110 latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\ |
110 latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\ |
121 & & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\ |
121 & & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\ |
122 & & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\ |
122 & & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\ |
123 & & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\ |
123 & & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\ |
124 \end{matharray} |
124 \end{matharray} |
125 |
125 |
126 The syntax of \mbox{\isa{string}} admits any characters, including |
126 The syntax of \hyperlink{syntax.string}{\mbox{\isa{string}}} admits any characters, including |
127 newlines; ``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) need to be escaped by a backslash; arbitrary |
127 newlines; ``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) need to be escaped by a backslash; arbitrary |
128 character codes may be specified as ``\verb|\|\isa{ddd}'', |
128 character codes may be specified as ``\verb|\|\isa{ddd}'', |
129 with three decimal digits. Alternative strings according to |
129 with three decimal digits. Alternative strings according to |
130 \mbox{\isa{altstring}} are analogous, using single back-quotes instead. |
130 \hyperlink{syntax.altstring}{\mbox{\isa{altstring}}} are analogous, using single back-quotes instead. |
131 The body of \mbox{\isa{verbatim}} may consist of any text not |
131 The body of \hyperlink{syntax.verbatim}{\mbox{\isa{verbatim}}} may consist of any text not |
132 containing ``\verb|*|\verb|}|''; this allows |
132 containing ``\verb|*|\verb|}|''; this allows |
133 convenient inclusion of quotes without further escapes. The greek |
133 convenient inclusion of quotes without further escapes. The greek |
134 letters do \emph{not} include \verb|\<lambda>|, which is already used |
134 letters do \emph{not} include \verb|\<lambda>|, which is already used |
135 differently in the meta-logic. |
135 differently in the meta-logic. |
136 |
136 |
408 |
408 |
409 \item named facts \isa{{\isachardoublequote}a{\isachardoublequote}}, |
409 \item named facts \isa{{\isachardoublequote}a{\isachardoublequote}}, |
410 |
410 |
411 \item selections from named facts \isa{{\isachardoublequote}a{\isacharparenleft}i{\isacharparenright}{\isachardoublequote}} or \isa{{\isachardoublequote}a{\isacharparenleft}j\ {\isacharminus}\ k{\isacharparenright}{\isachardoublequote}}, |
411 \item selections from named facts \isa{{\isachardoublequote}a{\isacharparenleft}i{\isacharparenright}{\isachardoublequote}} or \isa{{\isachardoublequote}a{\isacharparenleft}j\ {\isacharminus}\ k{\isacharparenright}{\isachardoublequote}}, |
412 |
412 |
413 \item literal fact propositions using \indexref{}{syntax}{altstring}\mbox{\isa{altstring}} syntax |
413 \item literal fact propositions using \indexref{}{syntax}{altstring}\hyperlink{syntax.altstring}{\mbox{\isa{altstring}}} syntax |
414 \verb|`|\isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}\verb|`| (see also method |
414 \verb|`|\isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}\verb|`| (see also method |
415 \indexref{}{method}{fact}\mbox{\isa{fact}} in \secref{sec:pure-meth-att}). |
415 \indexref{}{method}{fact}\hyperlink{method.fact}{\mbox{\isa{fact}}} in \secref{sec:pure-meth-att}). |
416 |
416 |
417 \end{enumerate} |
417 \end{enumerate} |
418 |
418 |
419 Any kind of theorem specification may include lists of attributes |
419 Any kind of theorem specification may include lists of attributes |
420 both on the left and right hand sides; attributes are applied to any |
420 both on the left and right hand sides; attributes are applied to any |
424 |
424 |
425 An extra pair of brackets around attributes (like ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbrackleft}simproc\ a{\isacharbrackright}{\isacharbrackright}{\isachardoublequote}}'') abbreviates a theorem reference involving an |
425 An extra pair of brackets around attributes (like ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbrackleft}simproc\ a{\isacharbrackright}{\isacharbrackright}{\isachardoublequote}}'') abbreviates a theorem reference involving an |
426 internal dummy fact, which will be ignored later on. So only the |
426 internal dummy fact, which will be ignored later on. So only the |
427 effect of the attribute on the background context will persist. |
427 effect of the attribute on the background context will persist. |
428 This form of in-place declarations is particularly useful with |
428 This form of in-place declarations is particularly useful with |
429 commands like \mbox{\isa{\isacommand{declare}}} and \mbox{\isa{\isacommand{using}}}. |
429 commands like \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} and \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}. |
430 |
430 |
431 \indexouternonterm{axmdecl}\indexouternonterm{thmdecl} |
431 \indexouternonterm{axmdecl}\indexouternonterm{thmdecl} |
432 \indexouternonterm{thmdef}\indexouternonterm{thmref} |
432 \indexouternonterm{thmdef}\indexouternonterm{thmref} |
433 \indexouternonterm{thmrefs}\indexouternonterm{selection} |
433 \indexouternonterm{thmrefs}\indexouternonterm{selection} |
434 \begin{rail} |
434 \begin{rail} |
488 complementary focus of \railnonterm{vars} versus |
488 complementary focus of \railnonterm{vars} versus |
489 \railnonterm{props}. In ``\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}}'' |
489 \railnonterm{props}. In ``\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}}'' |
490 the typing refers to all variables, while in \isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}} the naming refers to all propositions collectively. |
490 the typing refers to all variables, while in \isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}} the naming refers to all propositions collectively. |
491 Isar language elements that refer to \railnonterm{vars} or |
491 Isar language elements that refer to \railnonterm{vars} or |
492 \railnonterm{props} typically admit separate typings or namings via |
492 \railnonterm{props} typically admit separate typings or namings via |
493 another level of iteration, with explicit \indexref{}{keyword}{and}\mbox{\isa{\isakeyword{and}}} |
493 another level of iteration, with explicit \indexref{}{keyword}{and}\hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}} |
494 separators; e.g.\ see \mbox{\isa{\isacommand{fix}}} and \mbox{\isa{\isacommand{assume}}} in |
494 separators; e.g.\ see \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}} and \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} in |
495 \secref{sec:proof-context}.% |
495 \secref{sec:proof-context}.% |
496 \end{isamarkuptext}% |
496 \end{isamarkuptext}% |
497 \isamarkuptrue% |
497 \isamarkuptrue% |
498 % |
498 % |
499 \isamarkupsubsection{Antiquotations \label{sec:antiq}% |
499 \isamarkupsubsection{Antiquotations \label{sec:antiq}% |
500 } |
500 } |
501 \isamarkuptrue% |
501 \isamarkuptrue% |
502 % |
502 % |
503 \begin{isamarkuptext}% |
503 \begin{isamarkuptext}% |
504 \begin{matharray}{rcl} |
504 \begin{matharray}{rcl} |
505 \indexdef{}{antiquotation}{theory}\mbox{\isa{theory}} & : & \isarantiq \\ |
505 \indexdef{}{antiquotation}{theory}\hypertarget{antiquotation.theory}{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isarantiq \\ |
506 \indexdef{}{antiquotation}{thm}\mbox{\isa{thm}} & : & \isarantiq \\ |
506 \indexdef{}{antiquotation}{thm}\hypertarget{antiquotation.thm}{\hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}} & : & \isarantiq \\ |
507 \indexdef{}{antiquotation}{prop}\mbox{\isa{prop}} & : & \isarantiq \\ |
507 \indexdef{}{antiquotation}{prop}\hypertarget{antiquotation.prop}{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isarantiq \\ |
508 \indexdef{}{antiquotation}{term}\mbox{\isa{term}} & : & \isarantiq \\ |
508 \indexdef{}{antiquotation}{term}\hypertarget{antiquotation.term}{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}} & : & \isarantiq \\ |
509 \indexdef{}{antiquotation}{const}\mbox{\isa{const}} & : & \isarantiq \\ |
509 \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isarantiq \\ |
510 \indexdef{}{antiquotation}{abbrev}\mbox{\isa{abbrev}} & : & \isarantiq \\ |
510 \indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isarantiq \\ |
511 \indexdef{}{antiquotation}{typeof}\mbox{\isa{typeof}} & : & \isarantiq \\ |
511 \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isarantiq \\ |
512 \indexdef{}{antiquotation}{typ}\mbox{\isa{typ}} & : & \isarantiq \\ |
512 \indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isarantiq \\ |
513 \indexdef{}{antiquotation}{thm\_style}\mbox{\isa{thm{\isacharunderscore}style}} & : & \isarantiq \\ |
513 \indexdef{}{antiquotation}{thm\_style}\hypertarget{antiquotation.thm_style}{\hyperlink{antiquotation.thm_style}{\mbox{\isa{thm{\isacharunderscore}style}}}} & : & \isarantiq \\ |
514 \indexdef{}{antiquotation}{term\_style}\mbox{\isa{term{\isacharunderscore}style}} & : & \isarantiq \\ |
514 \indexdef{}{antiquotation}{term\_style}\hypertarget{antiquotation.term_style}{\hyperlink{antiquotation.term_style}{\mbox{\isa{term{\isacharunderscore}style}}}} & : & \isarantiq \\ |
515 \indexdef{}{antiquotation}{text}\mbox{\isa{text}} & : & \isarantiq \\ |
515 \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isarantiq \\ |
516 \indexdef{}{antiquotation}{goals}\mbox{\isa{goals}} & : & \isarantiq \\ |
516 \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isarantiq \\ |
517 \indexdef{}{antiquotation}{subgoals}\mbox{\isa{subgoals}} & : & \isarantiq \\ |
517 \indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isarantiq \\ |
518 \indexdef{}{antiquotation}{prf}\mbox{\isa{prf}} & : & \isarantiq \\ |
518 \indexdef{}{antiquotation}{prf}\hypertarget{antiquotation.prf}{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}} & : & \isarantiq \\ |
519 \indexdef{}{antiquotation}{full\_prf}\mbox{\isa{full{\isacharunderscore}prf}} & : & \isarantiq \\ |
519 \indexdef{}{antiquotation}{full\_prf}\hypertarget{antiquotation.full_prf}{\hyperlink{antiquotation.full_prf}{\mbox{\isa{full{\isacharunderscore}prf}}}} & : & \isarantiq \\ |
520 \indexdef{}{antiquotation}{ML}\mbox{\isa{ML}} & : & \isarantiq \\ |
520 \indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isarantiq \\ |
521 \indexdef{}{antiquotation}{ML\_type}\mbox{\isa{ML{\isacharunderscore}type}} & : & \isarantiq \\ |
521 \indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML_type}{\hyperlink{antiquotation.ML_type}{\mbox{\isa{ML{\isacharunderscore}type}}}} & : & \isarantiq \\ |
522 \indexdef{}{antiquotation}{ML\_struct}\mbox{\isa{ML{\isacharunderscore}struct}} & : & \isarantiq \\ |
522 \indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML_struct}{\hyperlink{antiquotation.ML_struct}{\mbox{\isa{ML{\isacharunderscore}struct}}}} & : & \isarantiq \\ |
523 \end{matharray} |
523 \end{matharray} |
524 |
524 |
525 The text body of formal comments (see also \secref{sec:comments}) |
525 The text body of formal comments (see also \secref{sec:comments}) |
526 may contain antiquotations of logical entities, such as theorems, |
526 may contain antiquotations of logical entities, such as theorems, |
527 terms and types, which are to be presented in the final output |
527 terms and types, which are to be presented in the final output |
577 context. |
577 context. |
578 |
578 |
579 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints theorems |
579 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints theorems |
580 \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. Note that attribute specifications |
580 \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. Note that attribute specifications |
581 may be included as well (see also \secref{sec:syn-att}); the |
581 may be included as well (see also \secref{sec:syn-att}); the |
582 \indexref{}{attribute}{no\_vars}\mbox{\isa{no{\isacharunderscore}vars}} rule (see \secref{sec:misc-meth-att}) would |
582 \indexref{}{attribute}{no\_vars}\hyperlink{attribute.no_vars}{\mbox{\isa{no{\isacharunderscore}vars}}} rule (see \secref{sec:misc-meth-att}) would |
583 be particularly useful to suppress printing of schematic variables. |
583 be particularly useful to suppress printing of schematic variables. |
584 |
584 |
585 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}}] prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}. |
585 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}}] prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}. |
586 |
586 |
587 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}}] prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}. |
587 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}}] prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}. |
699 \item[\isa{{\isachardoublequote}margin\ {\isacharequal}\ nat{\isachardoublequote}} and \isa{{\isachardoublequote}indent\ {\isacharequal}\ nat{\isachardoublequote}}] change the |
699 \item[\isa{{\isachardoublequote}margin\ {\isacharequal}\ nat{\isachardoublequote}} and \isa{{\isachardoublequote}indent\ {\isacharequal}\ nat{\isachardoublequote}}] change the |
700 margin or indentation for pretty printing of display material. |
700 margin or indentation for pretty printing of display material. |
701 |
701 |
702 \item[\isa{{\isachardoublequote}source\ {\isacharequal}\ bool{\isachardoublequote}}] prints the source text of the |
702 \item[\isa{{\isachardoublequote}source\ {\isacharequal}\ bool{\isachardoublequote}}] prints the source text of the |
703 antiquotation arguments, rather than the actual value. Note that |
703 antiquotation arguments, rather than the actual value. Note that |
704 this does not affect well-formedness checks of \mbox{\isa{thm}}, \mbox{\isa{term}}, etc. (only the \mbox{\isa{text}} antiquotation admits arbitrary output). |
704 this does not affect well-formedness checks of \hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. (only the \hyperlink{antiquotation.text}{\mbox{\isa{text}}} antiquotation admits arbitrary output). |
705 |
705 |
706 \item[\isa{{\isachardoublequote}goals{\isacharunderscore}limit\ {\isacharequal}\ nat{\isachardoublequote}}] determines the maximum number of |
706 \item[\isa{{\isachardoublequote}goals{\isacharunderscore}limit\ {\isacharequal}\ nat{\isachardoublequote}}] determines the maximum number of |
707 goals to be printed. |
707 goals to be printed. |
708 |
708 |
709 \item[\isa{{\isachardoublequote}locale\ {\isacharequal}\ name{\isachardoublequote}}] specifies an alternative locale |
709 \item[\isa{{\isachardoublequote}locale\ {\isacharequal}\ name{\isachardoublequote}}] specifies an alternative locale |
751 \medskip The Isabelle document preparation system (see also |
751 \medskip The Isabelle document preparation system (see also |
752 \cite{isabelle-sys}) allows tagged command regions to be presented |
752 \cite{isabelle-sys}) allows tagged command regions to be presented |
753 specifically, e.g.\ to fold proof texts, or drop parts of the text |
753 specifically, e.g.\ to fold proof texts, or drop parts of the text |
754 completely. |
754 completely. |
755 |
755 |
756 For example ``\mbox{\isa{\isacommand{by}}}~\isa{{\isachardoublequote}{\isacharpercent}invisible\ auto{\isachardoublequote}}'' would |
756 For example ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}invisible\ auto{\isachardoublequote}}'' would |
757 cause that piece of proof to be treated as \isa{invisible} instead |
757 cause that piece of proof to be treated as \isa{invisible} instead |
758 of \isa{{\isachardoublequote}proof{\isachardoublequote}} (the default), which may be either show or hidden |
758 of \isa{{\isachardoublequote}proof{\isachardoublequote}} (the default), which may be either show or hidden |
759 depending on the document setup. In contrast, ``\mbox{\isa{\isacommand{by}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ auto{\isachardoublequote}}'' would force this text to be shown |
759 depending on the document setup. In contrast, ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ auto{\isachardoublequote}}'' would force this text to be shown |
760 invariably. |
760 invariably. |
761 |
761 |
762 Explicit tag specifications within a proof apply to all subsequent |
762 Explicit tag specifications within a proof apply to all subsequent |
763 commands of the same level of nesting. For example, ``\mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ {\isasymdots}{\isachardoublequote}}~\mbox{\isa{\isacommand{qed}}}'' would force the |
763 commands of the same level of nesting. For example, ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ {\isasymdots}{\isachardoublequote}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}'' would force the |
764 whole sub-proof to be typeset as \isa{visible} (unless some of its |
764 whole sub-proof to be typeset as \isa{visible} (unless some of its |
765 parts are tagged differently).% |
765 parts are tagged differently).% |
766 \end{isamarkuptext}% |
766 \end{isamarkuptext}% |
767 \isamarkuptrue% |
767 \isamarkuptrue% |
768 % |
768 % |