wneuper/isa: comparison doc-src/IsarRef/Thy/document/Document

equal deleted inserted replaced

-:824d3f1d8de6
+:2080fe35abea
 Note that formal comments (\secref{sec:comments}) are similar to
 markup commands, but have a different status within Isabelle/Isar
 syntax.
 \begin{railoutput}
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
 \rail@bar
 \rail@term{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}}[]
 \rail@nextbar{1}
 \rail@term{\hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}}[]
 \rail@nextbar{2}
 \rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
 \rail@endbar
 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
 \rail@end
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
 \rail@bar
 \rail@term{\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}}[]
 \rail@nextbar{1}
 \rail@term{\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isaliteral{5F}{\isacharunderscore}}raw}}}}}[]
 \rail@nextbar{2}
 informal explanation is achieved, since terms and types appearing in
 antiquotations are checked within the current theory or proof
 context.
 \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}}}[]
 \rail@nont{\isa{antiquotation}}[]
 \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
 \rail@end
 \rail@begin{22}{\indexdef{}{syntax}{antiquotation}\hypertarget{syntax.antiquotation}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}}
 \begin{matharray}{rcl}
 \indexdef{}{antiquotation}{rail}\hypertarget{antiquotation.rail}{\hyperlink{antiquotation.rail}{\mbox{\isa{rail}}}} & : & \isa{antiquotation} \\
 \end{matharray}
 \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\isa{rail}}[]
 \rail@nont{\isa{string}}[]
 \rail@end
 \end{railoutput}
 example.
 The rail specification language is quoted here as Isabelle \hyperlink{syntax.string}{\mbox{\isa{string}}}; it has its own grammar given below.
 \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@plus
 \rail@bar
 \rail@nextbar{1}
 \rail@nont{\isa{rule}}[]
 \rail@endbar
 \begin{itemize}
 \item Empty \verb|()|
 \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@end
 \end{railoutput}
 \item Nonterminal \verb|A|
 \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@nont{\isa{A}}[]
 \rail@end
 \end{railoutput}
 \item Nonterminal via Isabelle antiquotation
 \verb|@{syntax method}|
 \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
 \rail@end
 \end{railoutput}
 \item Terminal \verb|'xyz'|
 \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\isa{xyz}}[]
 \rail@end
 \end{railoutput}
 \item Terminal in keyword style \verb|@'xyz'|
 \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\isa{\isakeyword{xyz}}}[]
 \rail@end
 \end{railoutput}
 \item Terminal via Isabelle antiquotation
 \verb|@@{method rule}|
 \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
 \rail@end
 \end{railoutput}
 \item Concatenation \verb|A B C|
 \begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
 \rail@nont{\isa{A}}[]
 \rail@nont{\isa{B}}[]
 \rail@nont{\isa{C}}[]
 \rail@end
 \end{railoutput}
 concatenation\footnote{Strictly speaking, this is only a single
 backslash, but the enclosing \hyperlink{syntax.string}{\mbox{\isa{string}}} syntax requires a
 second one for escaping.} \verb|A B C \\ D E F|
 \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@nont{\isa{A}}[]
 \rail@nont{\isa{B}}[]
 \rail@nont{\isa{C}}[]
 \rail@cr{2}
 \rail@nont{\isa{D}}[]
 \item Variants \verb|A |\verb,|,\verb| B |\verb,|,\verb| C|
 \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@nont{\isa{A}}[]
 \rail@nextbar{1}
 \rail@nont{\isa{B}}[]
 \rail@nextbar{2}
 \item Option \verb|A ?|
 \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@nextbar{1}
 \rail@nont{\isa{A}}[]
 \rail@endbar
 \rail@end
 \item Repetition \verb|A *|
 \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@plus
 \rail@nextplus{1}
 \rail@cnont{\isa{A}}[]
 \rail@endplus
 \rail@end
 \item Repetition with separator \verb|A * sep|
 \begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
 \rail@bar
 \rail@nextbar{1}
 \rail@plus
 \rail@nont{\isa{A}}[]
 \rail@nextplus{2}
 \item Strict repetition \verb|A +|
 \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@plus
 \rail@nont{\isa{A}}[]
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
 \item Strict repetition with separator \verb|A + sep|
 \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@plus
 \rail@nont{\isa{A}}[]
 \rail@nextplus{1}
 \rail@cnont{\isa{sep}}[]
 \rail@endplus
 \indexdef{}{command}{display\_drafts}\hypertarget{command.display-drafts}{\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isaliteral{5F}{\isacharunderscore}}drafts}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
 \indexdef{}{command}{print\_drafts}\hypertarget{command.print-drafts}{\hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}drafts}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
 \end{matharray}
 \begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
 \rail@bar
 \rail@term{\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isaliteral{5F}{\isacharunderscore}}drafts}}}}}[]
 \rail@nextbar{1}
 \rail@term{\hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}drafts}}}}}[]
 \rail@endbar

changeset 43535	2080fe35abea
parent 43529	8f5d5d71add0
child 43542	04dfffda5671