author | bulwahn |
Fri, 01 Jul 2011 10:45:51 +0200 | |
changeset 43613 | 7afbaf5a406b |
parent 42936 | 48a0a9db3453 |
child 43618 | 1c43134ff988 |
permissions | -rw-r--r-- |
27042 | 1 |
% |
2 |
\begin{isabellebody}% |
|
40406 | 3 |
\def\isabellecontext{Document{\isaliteral{5F}{\isacharunderscore}}Preparation}% |
27042 | 4 |
% |
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
40406 | 11 |
\ Document{\isaliteral{5F}{\isacharunderscore}}Preparation\isanewline |
42651 | 12 |
\isakeyword{imports}\ Base\ Main\isanewline |
27042 | 13 |
\isakeyword{begin}% |
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
21 |
\isamarkupchapter{Document preparation \label{ch:document-prep}% |
|
22 |
} |
|
23 |
\isamarkuptrue% |
|
24 |
% |
|
25 |
\begin{isamarkuptext}% |
|
28788 | 26 |
Isabelle/Isar provides a simple document preparation system |
27 |
based on regular {PDF-\LaTeX} technology, with full support for |
|
28 |
hyper-links and bookmarks. Thus the results are well suited for WWW |
|
29 |
browsing and as printed copies. |
|
27042 | 30 |
|
28788 | 31 |
\medskip Isabelle generates {\LaTeX} output while running a |
27042 | 32 |
\emph{logic session} (see also \cite{isabelle-sys}). Getting |
33 |
started with a working configuration for common situations is quite |
|
34 |
easy by using the Isabelle \verb|mkdir| and \verb|make| |
|
35 |
tools. First invoke |
|
36 |
\begin{ttbox} |
|
28505 | 37 |
isabelle mkdir Foo |
27042 | 38 |
\end{ttbox} |
28788 | 39 |
to initialize a separate directory for session \verb|Foo| (it |
40 |
is safe to experiment, since \verb|isabelle mkdir| never |
|
41 |
overwrites existing files). Ensure that \verb|Foo/ROOT.ML| |
|
27042 | 42 |
holds ML commands to load all theories required for this session; |
43 |
furthermore \verb|Foo/document/root.tex| should include any |
|
44 |
special {\LaTeX} macro packages required for your document (the |
|
45 |
default is usually sufficient as a start). |
|
46 |
||
47 |
The session is controlled by a separate \verb|IsaMakefile| |
|
48 |
(with crude source dependencies by default). This file is located |
|
49 |
one level up from the \verb|Foo| directory location. Now |
|
50 |
invoke |
|
51 |
\begin{ttbox} |
|
28505 | 52 |
isabelle make Foo |
27042 | 53 |
\end{ttbox} |
54 |
to run the \verb|Foo| session, with browser information and |
|
55 |
document preparation enabled. Unless any errors are reported by |
|
56 |
Isabelle or {\LaTeX}, the output will appear inside the directory |
|
28788 | 57 |
defined by the \verb|ISABELLE_BROWSER_INFO| setting (as |
58 |
reported by the batch job in verbose mode). |
|
27042 | 59 |
|
60 |
\medskip You may also consider to tune the \verb|usedir| |
|
28788 | 61 |
options in \verb|IsaMakefile|, for example to switch the output |
62 |
format between \verb|pdf| and \verb|dvi|, or activate the |
|
27042 | 63 |
\verb|-D| option to retain a second copy of the generated |
28788 | 64 |
{\LaTeX} sources (for manual inspection or separate runs of |
65 |
\hyperlink{executable.latex}{\mbox{\isa{\isatt{latex}}}}). |
|
27042 | 66 |
|
67 |
\medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys} |
|
68 |
for further details on Isabelle logic sessions and theory |
|
69 |
presentation. The Isabelle/HOL tutorial \cite{isabelle-hol-book} |
|
28788 | 70 |
also covers theory presentation to some extent.% |
27042 | 71 |
\end{isamarkuptext}% |
72 |
\isamarkuptrue% |
|
73 |
% |
|
74 |
\isamarkupsection{Markup commands \label{sec:markup}% |
|
75 |
} |
|
76 |
\isamarkuptrue% |
|
77 |
% |
|
78 |
\begin{isamarkuptext}% |
|
79 |
\begin{matharray}{rcl} |
|
40406 | 80 |
\indexdef{}{command}{header}\hypertarget{command.header}{\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}toplevel\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ toplevel{\isaliteral{22}{\isachardoublequote}}} \\[0.5ex] |
81 |
\indexdef{}{command}{chapter}\hypertarget{command.chapter}{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
82 |
\indexdef{}{command}{section}\hypertarget{command.section}{\hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
83 |
\indexdef{}{command}{subsection}\hypertarget{command.subsection}{\hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
84 |
\indexdef{}{command}{subsubsection}\hypertarget{command.subsubsection}{\hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
85 |
\indexdef{}{command}{text}\hypertarget{command.text}{\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
86 |
\indexdef{}{command}{text\_raw}\hypertarget{command.text-raw}{\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isaliteral{5F}{\isacharunderscore}}raw}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\[0.5ex] |
|
87 |
\indexdef{}{command}{sect}\hypertarget{command.sect}{\hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{22}{\isachardoublequote}}} \\ |
|
88 |
\indexdef{}{command}{subsect}\hypertarget{command.subsect}{\hyperlink{command.subsect}{\mbox{\isa{\isacommand{subsect}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{22}{\isachardoublequote}}} \\ |
|
89 |
\indexdef{}{command}{subsubsect}\hypertarget{command.subsubsect}{\hyperlink{command.subsubsect}{\mbox{\isa{\isacommand{subsubsect}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{22}{\isachardoublequote}}} \\ |
|
90 |
\indexdef{}{command}{txt}\hypertarget{command.txt}{\hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{22}{\isachardoublequote}}} \\ |
|
91 |
\indexdef{}{command}{txt\_raw}\hypertarget{command.txt-raw}{\hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isaliteral{5F}{\isacharunderscore}}raw}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{22}{\isachardoublequote}}} \\ |
|
27042 | 92 |
\end{matharray} |
93 |
||
28788 | 94 |
Markup commands provide a structured way to insert text into the |
95 |
document generated from a theory. Each markup command takes a |
|
96 |
single \hyperlink{syntax.text}{\mbox{\isa{text}}} argument, which is passed as argument to a |
|
97 |
corresponding {\LaTeX} macro. The default macros provided by |
|
40802 | 98 |
\verb|~~/lib/texinputs/isabelle.sty| can be redefined according |
28788 | 99 |
to the needs of the underlying document and {\LaTeX} styles. |
100 |
||
101 |
Note that formal comments (\secref{sec:comments}) are similar to |
|
102 |
markup commands, but have a different status within Isabelle/Isar |
|
103 |
syntax. |
|
27042 | 104 |
|
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
105 |
\begin{railoutput} |
42662 | 106 |
\rail@begin{5}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
107 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
108 |
\rail@term{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
109 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
110 |
\rail@term{\hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
111 |
\rail@nextbar{2} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
112 |
\rail@term{\hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
113 |
\rail@nextbar{3} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
114 |
\rail@term{\hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
115 |
\rail@nextbar{4} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
116 |
\rail@term{\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
117 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
118 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
119 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
120 |
\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
121 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
122 |
\rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
123 |
\rail@end |
42662 | 124 |
\rail@begin{7}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
125 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
126 |
\rail@term{\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
127 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
128 |
\rail@term{\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isaliteral{5F}{\isacharunderscore}}raw}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
129 |
\rail@nextbar{2} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
130 |
\rail@term{\hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
131 |
\rail@nextbar{3} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
132 |
\rail@term{\hyperlink{command.subsect}{\mbox{\isa{\isacommand{subsect}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
133 |
\rail@nextbar{4} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
134 |
\rail@term{\hyperlink{command.subsubsect}{\mbox{\isa{\isacommand{subsubsect}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
135 |
\rail@nextbar{5} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
136 |
\rail@term{\hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
137 |
\rail@nextbar{6} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
138 |
\rail@term{\hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isaliteral{5F}{\isacharunderscore}}raw}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
139 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
140 |
\rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
141 |
\rail@end |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
142 |
\end{railoutput} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
143 |
|
27042 | 144 |
|
28788 | 145 |
\begin{description} |
27042 | 146 |
|
28788 | 147 |
\item \hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} provides plain text markup just preceding |
148 |
the formal beginning of a theory. The corresponding {\LaTeX} macro |
|
149 |
is \verb|\isamarkupheader|, which acts like \hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}} by default. |
|
27052 | 150 |
|
28788 | 151 |
\item \hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}, \hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}, \hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}, |
152 |
and \hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}} mark chapter and section headings |
|
153 |
within the main theory body or local theory targets. The |
|
154 |
corresponding {\LaTeX} macros are \verb|\isamarkupchapter|, |
|
155 |
\verb|\isamarkupsection|, \verb|\isamarkupsubsection| etc. |
|
27042 | 156 |
|
28788 | 157 |
\item \hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}, \hyperlink{command.subsect}{\mbox{\isa{\isacommand{subsect}}}}, and \hyperlink{command.subsubsect}{\mbox{\isa{\isacommand{subsubsect}}}} |
158 |
mark section headings within proofs. The corresponding {\LaTeX} |
|
159 |
macros are \verb|\isamarkupsect|, \verb|\isamarkupsubsect| etc. |
|
27042 | 160 |
|
28788 | 161 |
\item \hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}} and \hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}} specify paragraphs of plain |
40406 | 162 |
text. This corresponds to a {\LaTeX} environment \verb|\begin{isamarkuptext}| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|\end{isamarkuptext}| etc. |
27042 | 163 |
|
40406 | 164 |
\item \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isaliteral{5F}{\isacharunderscore}}raw}}}} and \hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isaliteral{5F}{\isacharunderscore}}raw}}}} insert {\LaTeX} |
28788 | 165 |
source into the output, without additional markup. Thus the full |
166 |
range of document manipulations becomes available, at the risk of |
|
167 |
messing up document output. |
|
27042 | 168 |
|
28788 | 169 |
\end{description} |
27042 | 170 |
|
40406 | 171 |
Except for \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isaliteral{5F}{\isacharunderscore}}raw}}}} and \hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isaliteral{5F}{\isacharunderscore}}raw}}}}, the text |
28788 | 172 |
passed to any of the above markup commands may refer to formal |
173 |
entities via \emph{document antiquotations}, see also |
|
174 |
\secref{sec:antiq}. These are interpreted in the present theory or |
|
40406 | 175 |
proof context, or the named \isa{{\isaliteral{22}{\isachardoublequote}}target{\isaliteral{22}{\isachardoublequote}}}. |
27042 | 176 |
|
177 |
\medskip The proof markup commands closely resemble those for theory |
|
178 |
specifications, but have a different formal status and produce |
|
28788 | 179 |
different {\LaTeX} macros. The default definitions coincide for |
180 |
analogous commands such as \hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}} and \hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}.% |
|
27042 | 181 |
\end{isamarkuptext}% |
182 |
\isamarkuptrue% |
|
183 |
% |
|
28788 | 184 |
\isamarkupsection{Document Antiquotations \label{sec:antiq}% |
27042 | 185 |
} |
186 |
\isamarkuptrue% |
|
187 |
% |
|
188 |
\begin{isamarkuptext}% |
|
189 |
\begin{matharray}{rcl} |
|
28788 | 190 |
\indexdef{}{antiquotation}{theory}\hypertarget{antiquotation.theory}{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isa{antiquotation} \\ |
191 |
\indexdef{}{antiquotation}{thm}\hypertarget{antiquotation.thm}{\hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}} & : & \isa{antiquotation} \\ |
|
192 |
\indexdef{}{antiquotation}{lemma}\hypertarget{antiquotation.lemma}{\hyperlink{antiquotation.lemma}{\mbox{\isa{lemma}}}} & : & \isa{antiquotation} \\ |
|
193 |
\indexdef{}{antiquotation}{prop}\hypertarget{antiquotation.prop}{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isa{antiquotation} \\ |
|
194 |
\indexdef{}{antiquotation}{term}\hypertarget{antiquotation.term}{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}} & : & \isa{antiquotation} \\ |
|
40406 | 195 |
\indexdef{}{antiquotation}{term\_type}\hypertarget{antiquotation.term-type}{\hyperlink{antiquotation.term-type}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}type}}}} & : & \isa{antiquotation} \\ |
32898
e871d897969c
term styles also cover antiquotations term_type and typeof
haftmann
parents:
32893
diff
changeset
|
196 |
\indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isa{antiquotation} \\ |
28788 | 197 |
\indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isa{antiquotation} \\ |
198 |
\indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isa{antiquotation} \\ |
|
199 |
\indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isa{antiquotation} \\ |
|
39437 | 200 |
\indexdef{}{antiquotation}{type}\hypertarget{antiquotation.type}{\hyperlink{antiquotation.type}{\mbox{\isa{type}}}} & : & \isa{antiquotation} \\ |
201 |
\indexdef{}{antiquotation}{class}\hypertarget{antiquotation.class}{\hyperlink{antiquotation.class}{\mbox{\isa{class}}}} & : & \isa{antiquotation} \\ |
|
28788 | 202 |
\indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isa{antiquotation} \\ |
203 |
\indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isa{antiquotation} \\ |
|
204 |
\indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isa{antiquotation} \\ |
|
205 |
\indexdef{}{antiquotation}{prf}\hypertarget{antiquotation.prf}{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}} & : & \isa{antiquotation} \\ |
|
40406 | 206 |
\indexdef{}{antiquotation}{full\_prf}\hypertarget{antiquotation.full-prf}{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isaliteral{5F}{\isacharunderscore}}prf}}}} & : & \isa{antiquotation} \\ |
28788 | 207 |
\indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isa{antiquotation} \\ |
40406 | 208 |
\indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML-type}{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}type}}}} & : & \isa{antiquotation} \\ |
209 |
\indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML-struct}{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}struct}}}} & : & \isa{antiquotation} \\ |
|
40802 | 210 |
\indexdef{}{antiquotation}{file}\hypertarget{antiquotation.file}{\hyperlink{antiquotation.file}{\mbox{\isa{file}}}} & : & \isa{antiquotation} \\ |
27042 | 211 |
\end{matharray} |
212 |
||
28788 | 213 |
The overall content of an Isabelle/Isar theory may alternate between |
214 |
formal and informal text. The main body consists of formal |
|
215 |
specification and proof commands, interspersed with markup commands |
|
216 |
(\secref{sec:markup}) or document comments (\secref{sec:comments}). |
|
217 |
The argument of markup commands quotes informal text to be printed |
|
218 |
in the resulting document, but may again refer to formal entities |
|
219 |
via \emph{document antiquotations}. |
|
27042 | 220 |
|
40406 | 221 |
For example, embedding of ``\isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}term\ {\isaliteral{5B}{\isacharbrackleft}}show{\isaliteral{5F}{\isacharunderscore}}types{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{22}{\isachardoublequote}}f\ x\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2B}{\isacharplus}}\ x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7D}{\isacharbraceright}}}'' |
28788 | 222 |
within a text block makes |
223 |
\isa{{\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharplus}\ x} appear in the final {\LaTeX} document. |
|
224 |
||
225 |
Antiquotations usually spare the author tedious typing of logical |
|
226 |
entities in full detail. Even more importantly, some degree of |
|
227 |
consistency-checking between the main body of formal text and its |
|
228 |
informal explanation is achieved, since terms and types appearing in |
|
229 |
antiquotations are checked within the current theory or proof |
|
230 |
context. |
|
27042 | 231 |
|
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
232 |
\begin{railoutput} |
42662 | 233 |
\rail@begin{1}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
234 |
\rail@term{\isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
235 |
\rail@nont{\isa{antiquotation}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
236 |
\rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
237 |
\rail@end |
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
238 |
\rail@begin{23}{\indexdef{}{syntax}{antiquotation}\hypertarget{syntax.antiquotation}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
239 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
240 |
\rail@term{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
241 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
242 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
243 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
244 |
\rail@term{\hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
245 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
246 |
\rail@nont{\isa{styles}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
247 |
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
248 |
\rail@nextbar{2} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
249 |
\rail@term{\hyperlink{antiquotation.lemma}{\mbox{\isa{lemma}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
250 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
251 |
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
252 |
\rail@term{\isa{\isakeyword{by}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
253 |
\rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[] |
42617 | 254 |
\rail@bar |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
255 |
\rail@nextbar{3} |
42617 | 256 |
\rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[] |
257 |
\rail@endbar |
|
258 |
\rail@nextbar{4} |
|
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
259 |
\rail@term{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
260 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
261 |
\rail@nont{\isa{styles}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
262 |
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[] |
42617 | 263 |
\rail@nextbar{5} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
264 |
\rail@term{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
265 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
266 |
\rail@nont{\isa{styles}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
267 |
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] |
42617 | 268 |
\rail@nextbar{6} |
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
269 |
\rail@term{\hyperlink{antiquotation.value}{\mbox{\isa{value}}}}[] |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
270 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
271 |
\rail@nont{\isa{styles}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
272 |
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
273 |
\rail@nextbar{7} |
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
274 |
\rail@term{\hyperlink{antiquotation.term-type}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}type}}}}[] |
42617 | 275 |
\rail@nont{\isa{options}}[] |
276 |
\rail@nont{\isa{styles}}[] |
|
277 |
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] |
|
278 |
\rail@nextbar{8} |
|
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
279 |
\rail@term{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}}[] |
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
280 |
\rail@nont{\isa{options}}[] |
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
281 |
\rail@nont{\isa{styles}}[] |
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
282 |
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] |
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
283 |
\rail@nextbar{9} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
284 |
\rail@term{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
285 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
286 |
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] |
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
287 |
\rail@nextbar{10} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
288 |
\rail@term{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
289 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
290 |
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] |
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
291 |
\rail@nextbar{11} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
292 |
\rail@term{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
293 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
294 |
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[] |
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
295 |
\rail@nextbar{12} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
296 |
\rail@term{\hyperlink{antiquotation.type}{\mbox{\isa{type}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
297 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
298 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
299 |
\rail@nextbar{13} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
300 |
\rail@term{\hyperlink{antiquotation.class}{\mbox{\isa{class}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
301 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
302 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
42617 | 303 |
\rail@nextbar{14} |
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
304 |
\rail@term{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}}[] |
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
305 |
\rail@nont{\isa{options}}[] |
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
306 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
307 |
\rail@nextbar{15} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
308 |
\rail@term{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
309 |
\rail@nont{\isa{options}}[] |
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
310 |
\rail@nextbar{16} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
311 |
\rail@term{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
312 |
\rail@nont{\isa{options}}[] |
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
313 |
\rail@nextbar{17} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
314 |
\rail@term{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
315 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
316 |
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] |
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
317 |
\rail@nextbar{18} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
318 |
\rail@term{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isaliteral{5F}{\isacharunderscore}}prf}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
319 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
320 |
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] |
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
321 |
\rail@nextbar{19} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
322 |
\rail@term{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
323 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
324 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
325 |
\rail@nextbar{20} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
326 |
\rail@term{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}type}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
327 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
328 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
329 |
\rail@nextbar{21} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
330 |
\rail@term{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}struct}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
331 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
332 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
333 |
\rail@nextbar{22} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
334 |
\rail@term{\hyperlink{antiquotation.file}{\mbox{\isa{file}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
335 |
\rail@nont{\isa{options}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
336 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
337 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
338 |
\rail@end |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
339 |
\rail@begin{3}{\isa{options}} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
340 |
\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
341 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
342 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
343 |
\rail@plus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
344 |
\rail@nont{\isa{option}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
345 |
\rail@nextplus{2} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
346 |
\rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
347 |
\rail@endplus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
348 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
349 |
\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
350 |
\rail@end |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
351 |
\rail@begin{2}{\isa{option}} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
352 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
353 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
354 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
355 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
356 |
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
357 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
358 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
359 |
\rail@end |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
360 |
\rail@begin{2}{\isa{styles}} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
361 |
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
362 |
\rail@plus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
363 |
\rail@nont{\isa{style}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
364 |
\rail@nextplus{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
365 |
\rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
366 |
\rail@endplus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
367 |
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
368 |
\rail@end |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
369 |
\rail@begin{2}{\isa{style}} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
370 |
\rail@plus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
371 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
372 |
\rail@nextplus{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
373 |
\rail@endplus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
374 |
\rail@end |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
375 |
\end{railoutput} |
42617 | 376 |
|
27042 | 377 |
|
378 |
Note that the syntax of antiquotations may \emph{not} include source |
|
40406 | 379 |
comments \verb|(*|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}~\verb|*)| nor verbatim |
380 |
text \verb|{|\verb|*|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}~\verb|*|\verb|}|. |
|
27042 | 381 |
|
28788 | 382 |
\begin{description} |
27042 | 383 |
|
40406 | 384 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}theory\ A{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints the name \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}, which is |
27042 | 385 |
guaranteed to refer to a valid ancestor theory in the current |
386 |
context. |
|
387 |
||
40406 | 388 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}thm\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints theorems \isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}. |
28788 | 389 |
Full fact expressions are allowed here, including attributes |
390 |
(\secref{sec:syn-att}). |
|
391 |
||
40406 | 392 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}prop\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints a well-typed proposition \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}}. |
27042 | 393 |
|
40406 | 394 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}lemma\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ by\ m{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} proves a well-typed proposition |
395 |
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} by method \isa{m} and prints the original \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}}. |
|
27453 | 396 |
|
40406 | 397 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}term\ t{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints a well-typed term \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}}. |
43613
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
398 |
|
7afbaf5a406b
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn
parents:
42936
diff
changeset
|
399 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}value\ t{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} evaluates a term \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} and prints its result. |
27042 | 400 |
|
40406 | 401 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}term{\isaliteral{5F}{\isacharunderscore}}type\ t{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints a well-typed term \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} |
32898
e871d897969c
term styles also cover antiquotations term_type and typeof
haftmann
parents:
32893
diff
changeset
|
402 |
annotated with its type. |
e871d897969c
term styles also cover antiquotations term_type and typeof
haftmann
parents:
32893
diff
changeset
|
403 |
|
40406 | 404 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}typeof\ t{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints the type of a well-typed term |
405 |
\isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}}. |
|
32898
e871d897969c
term styles also cover antiquotations term_type and typeof
haftmann
parents:
32893
diff
changeset
|
406 |
|
40406 | 407 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}const\ c{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints a logical or syntactic constant |
408 |
\isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}}. |
|
27042 | 409 |
|
40406 | 410 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}abbrev\ c\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints a constant abbreviation |
411 |
\isa{{\isaliteral{22}{\isachardoublequote}}c\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ rhs{\isaliteral{22}{\isachardoublequote}}} as defined in the current context. |
|
39437 | 412 |
|
40406 | 413 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}typ\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints a well-formed type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}. |
39437 | 414 |
|
40406 | 415 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}type\ {\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints a (logical or syntactic) type |
416 |
constructor \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{22}{\isachardoublequote}}}. |
|
39437 | 417 |
|
40406 | 418 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}class\ c{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints a class \isa{c}. |
39437 | 419 |
|
40406 | 420 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}text\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints uninterpreted source text \isa{s}. This is particularly useful to print portions of text according |
28788 | 421 |
to the Isabelle document style, without demanding well-formedness, |
422 |
e.g.\ small pieces of terms that should not be parsed or |
|
423 |
type-checked yet. |
|
27042 | 424 |
|
40406 | 425 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}goals{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints the current \emph{dynamic} goal |
27042 | 426 |
state. This is mainly for support of tactic-emulation scripts |
28788 | 427 |
within Isar. Presentation of goal states does not conform to the |
428 |
idea of human-readable proof documents! |
|
27042 | 429 |
|
28788 | 430 |
When explaining proofs in detail it is usually better to spell out |
431 |
the reasoning via proper Isar proof commands, instead of peeking at |
|
432 |
the internal machine configuration. |
|
27042 | 433 |
|
40406 | 434 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}subgoals{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} is similar to \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}goals{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, but |
27042 | 435 |
does not print the main goal. |
436 |
||
40406 | 437 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}prf\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints the (compact) proof terms |
438 |
corresponding to the theorems \isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}. Note that this |
|
28788 | 439 |
requires proof terms to be switched on for the current logic |
440 |
session. |
|
27042 | 441 |
|
40406 | 442 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}full{\isaliteral{5F}{\isacharunderscore}}prf\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} is like \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}prf\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, but prints the full proof terms, i.e.\ also displays |
28788 | 443 |
information omitted in the compact proof term, which is denoted by |
40406 | 444 |
``\isa{{\isaliteral{5F}{\isacharunderscore}}}'' placeholders there. |
27042 | 445 |
|
40406 | 446 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ML\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ML{\isaliteral{5F}{\isacharunderscore}}type\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ML{\isaliteral{5F}{\isacharunderscore}}struct\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} check text \isa{s} as ML value, type, and |
28788 | 447 |
structure, respectively. The source is printed verbatim. |
27042 | 448 |
|
40802 | 449 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}file\ path{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} checks that \isa{{\isaliteral{22}{\isachardoublequote}}path{\isaliteral{22}{\isachardoublequote}}} refers to a |
450 |
file (or directory) and prints it verbatim. |
|
451 |
||
28788 | 452 |
\end{description}% |
453 |
\end{isamarkuptext}% |
|
454 |
\isamarkuptrue% |
|
455 |
% |
|
42936 | 456 |
\isamarkupsubsection{Styled antiquotations% |
28788 | 457 |
} |
458 |
\isamarkuptrue% |
|
459 |
% |
|
460 |
\begin{isamarkuptext}% |
|
32893 | 461 |
The antiquotations \isa{thm}, \isa{prop} and \isa{term} admit an extra \emph{style} specification to modify the |
462 |
printed result. A style is specified by a name with a possibly |
|
463 |
empty number of arguments; multiple styles can be sequenced with |
|
464 |
commas. The following standard styles are available: |
|
27042 | 465 |
|
28788 | 466 |
\begin{description} |
27042 | 467 |
|
28788 | 468 |
\item \isa{lhs} extracts the first argument of any application |
469 |
form with at least two arguments --- typically meta-level or |
|
27042 | 470 |
object-level equality, or any other binary relation. |
471 |
||
28788 | 472 |
\item \isa{rhs} is like \isa{lhs}, but extracts the second |
27042 | 473 |
argument. |
474 |
||
40406 | 475 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}concl{\isaliteral{22}{\isachardoublequote}}} extracts the conclusion \isa{C} from a rule |
476 |
in Horn-clause normal form \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequote}}}. |
|
27042 | 477 |
|
40406 | 478 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}prem{\isaliteral{22}{\isachardoublequote}}} \isa{n} extract premise number |
479 |
\isa{{\isaliteral{22}{\isachardoublequote}}n{\isaliteral{22}{\isachardoublequote}}} from from a rule in Horn-clause |
|
480 |
normal form \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequote}}} |
|
27042 | 481 |
|
28788 | 482 |
\end{description}% |
483 |
\end{isamarkuptext}% |
|
484 |
\isamarkuptrue% |
|
485 |
% |
|
42936 | 486 |
\isamarkupsubsection{General options% |
28788 | 487 |
} |
488 |
\isamarkuptrue% |
|
489 |
% |
|
490 |
\begin{isamarkuptext}% |
|
491 |
The following options are available to tune the printed output |
|
492 |
of antiquotations. Note that many of these coincide with global ML |
|
493 |
flags of the same names. |
|
27042 | 494 |
|
28788 | 495 |
\begin{description} |
27042 | 496 |
|
40406 | 497 |
\item \indexdef{}{antiquotation option}{show\_types}\hypertarget{antiquotation option.show-types}{\hyperlink{antiquotation option.show-types}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}types}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} and |
498 |
\indexdef{}{antiquotation option}{show\_sorts}\hypertarget{antiquotation option.show-sorts}{\hyperlink{antiquotation option.show-sorts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}sorts}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} control |
|
30397 | 499 |
printing of explicit type and sort constraints. |
27042 | 500 |
|
40406 | 501 |
\item \indexdef{}{antiquotation option}{show\_structs}\hypertarget{antiquotation option.show-structs}{\hyperlink{antiquotation option.show-structs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}structs}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} |
30397 | 502 |
controls printing of implicit structures. |
27042 | 503 |
|
40879
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40802
diff
changeset
|
504 |
\item \indexdef{}{antiquotation option}{show\_abbrevs}\hypertarget{antiquotation option.show-abbrevs}{\hyperlink{antiquotation option.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} |
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40802
diff
changeset
|
505 |
controls folding of abbreviations. |
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40802
diff
changeset
|
506 |
|
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42662
diff
changeset
|
507 |
\item \indexdef{}{antiquotation option}{names\_long}\hypertarget{antiquotation option.names-long}{\hyperlink{antiquotation option.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} forces |
30397 | 508 |
names of types and constants etc.\ to be printed in their fully |
509 |
qualified internal form. |
|
27042 | 510 |
|
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42662
diff
changeset
|
511 |
\item \indexdef{}{antiquotation option}{names\_short}\hypertarget{antiquotation option.names-short}{\hyperlink{antiquotation option.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} |
30397 | 512 |
forces names of types and constants etc.\ to be printed unqualified. |
513 |
Note that internalizing the output again in the current context may |
|
514 |
well yield a different result. |
|
27042 | 515 |
|
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42662
diff
changeset
|
516 |
\item \indexdef{}{antiquotation option}{names\_unique}\hypertarget{antiquotation option.names-unique}{\hyperlink{antiquotation option.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} |
30397 | 517 |
determines whether the printed version of qualified names should be |
518 |
made sufficiently long to avoid overlap with names declared further |
|
519 |
back. Set to \isa{false} for more concise output. |
|
27042 | 520 |
|
40406 | 521 |
\item \indexdef{}{antiquotation option}{eta\_contract}\hypertarget{antiquotation option.eta-contract}{\hyperlink{antiquotation option.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} |
522 |
prints terms in \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-contracted form. |
|
27042 | 523 |
|
40406 | 524 |
\item \indexdef{}{antiquotation option}{display}\hypertarget{antiquotation option.display}{\hyperlink{antiquotation option.display}{\mbox{\isa{display}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} indicates |
30397 | 525 |
if the text is to be output as multi-line ``display material'', |
526 |
rather than a small piece of text without line breaks (which is the |
|
527 |
default). |
|
27042 | 528 |
|
28788 | 529 |
In this mode the embedded entities are printed in the same style as |
530 |
the main theory text. |
|
531 |
||
40406 | 532 |
\item \indexdef{}{antiquotation option}{break}\hypertarget{antiquotation option.break}{\hyperlink{antiquotation option.break}{\mbox{\isa{break}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} controls |
30397 | 533 |
line breaks in non-display material. |
27042 | 534 |
|
40406 | 535 |
\item \indexdef{}{antiquotation option}{quotes}\hypertarget{antiquotation option.quotes}{\hyperlink{antiquotation option.quotes}{\mbox{\isa{quotes}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} indicates |
30397 | 536 |
if the output should be enclosed in double quotes. |
27042 | 537 |
|
40406 | 538 |
\item \indexdef{}{antiquotation option}{mode}\hypertarget{antiquotation option.mode}{\hyperlink{antiquotation option.mode}{\mbox{\isa{mode}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ name{\isaliteral{22}{\isachardoublequote}}} adds \isa{name} to the print mode to be used for presentation. Note that the |
30397 | 539 |
standard setup for {\LaTeX} output is already present by default, |
540 |
including the modes \isa{latex} and \isa{xsymbols}. |
|
27042 | 541 |
|
40406 | 542 |
\item \indexdef{}{antiquotation option}{margin}\hypertarget{antiquotation option.margin}{\hyperlink{antiquotation option.margin}{\mbox{\isa{margin}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ nat{\isaliteral{22}{\isachardoublequote}}} and |
543 |
\indexdef{}{antiquotation option}{indent}\hypertarget{antiquotation option.indent}{\hyperlink{antiquotation option.indent}{\mbox{\isa{indent}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ nat{\isaliteral{22}{\isachardoublequote}}} change the margin |
|
30397 | 544 |
or indentation for pretty printing of display material. |
27042 | 545 |
|
40406 | 546 |
\item \indexdef{}{antiquotation option}{goals\_limit}\hypertarget{antiquotation option.goals-limit}{\hyperlink{antiquotation option.goals-limit}{\mbox{\isa{goals{\isaliteral{5F}{\isacharunderscore}}limit}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ nat{\isaliteral{22}{\isachardoublequote}}} |
30397 | 547 |
determines the maximum number of goals to be printed (for goal-based |
548 |
antiquotation). |
|
27042 | 549 |
|
40406 | 550 |
\item \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} prints the |
30397 | 551 |
original source text of the antiquotation arguments, rather than its |
552 |
internal representation. Note that formal checking of |
|
553 |
\hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. is still |
|
554 |
enabled; use the \hyperlink{antiquotation.text}{\mbox{\isa{text}}} antiquotation for unchecked |
|
555 |
output. |
|
28788 | 556 |
|
40406 | 557 |
Regular \isa{{\isaliteral{22}{\isachardoublequote}}term{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}typ{\isaliteral{22}{\isachardoublequote}}} antiquotations with \isa{{\isaliteral{22}{\isachardoublequote}}source\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{22}{\isachardoublequote}}} involve a full round-trip from the original source |
28788 | 558 |
to an internalized logical entity back to a source form, according |
559 |
to the syntax of the current context. Thus the printed output is |
|
560 |
not under direct control of the author, it may even fluctuate a bit |
|
561 |
as the underlying theory is changed later on. |
|
562 |
||
42626 | 563 |
In contrast, \hyperlink{antiquotation option.source}{\mbox{\isa{source}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{22}{\isachardoublequote}}} |
30397 | 564 |
admits direct printing of the given source text, with the desirable |
565 |
well-formedness check in the background, but without modification of |
|
566 |
the printed text. |
|
28788 | 567 |
|
568 |
\end{description} |
|
27042 | 569 |
|
40406 | 570 |
For boolean flags, ``\isa{{\isaliteral{22}{\isachardoublequote}}name\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{22}{\isachardoublequote}}}'' may be abbreviated as |
27042 | 571 |
``\isa{name}''. All of the above flags are disabled by default, |
28788 | 572 |
unless changed from ML, say in the \verb|ROOT.ML| of the |
573 |
logic session.% |
|
27042 | 574 |
\end{isamarkuptext}% |
575 |
\isamarkuptrue% |
|
576 |
% |
|
28788 | 577 |
\isamarkupsection{Markup via command tags \label{sec:tags}% |
27042 | 578 |
} |
579 |
\isamarkuptrue% |
|
580 |
% |
|
581 |
\begin{isamarkuptext}% |
|
28788 | 582 |
Each Isabelle/Isar command may be decorated by additional |
583 |
presentation tags, to indicate some modification in the way it is |
|
584 |
printed in the document. |
|
27042 | 585 |
|
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
586 |
\begin{railoutput} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
587 |
\rail@begin{2}{\indexdef{}{syntax}{tags}\hypertarget{syntax.tags}{\hyperlink{syntax.tags}{\mbox{\isa{tags}}}}} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
588 |
\rail@plus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
589 |
\rail@nextplus{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
590 |
\rail@cnont{\isa{tag}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
591 |
\rail@endplus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
592 |
\rail@end |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
593 |
\rail@begin{2}{\isa{tag}} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
594 |
\rail@term{\isa{{\isaliteral{25}{\isacharpercent}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
595 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
596 |
\rail@nont{\hyperlink{syntax.ident}{\mbox{\isa{ident}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
597 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
598 |
\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
599 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
600 |
\rail@end |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
601 |
\end{railoutput} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
602 |
|
27042 | 603 |
|
28788 | 604 |
Some tags are pre-declared for certain classes of commands, serving |
605 |
as default markup if no tags are given in the text: |
|
27042 | 606 |
|
28788 | 607 |
\medskip |
27042 | 608 |
\begin{tabular}{ll} |
40406 | 609 |
\isa{{\isaliteral{22}{\isachardoublequote}}theory{\isaliteral{22}{\isachardoublequote}}} & theory begin/end \\ |
610 |
\isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{22}{\isachardoublequote}}} & all proof commands \\ |
|
611 |
\isa{{\isaliteral{22}{\isachardoublequote}}ML{\isaliteral{22}{\isachardoublequote}}} & all commands involving ML code \\ |
|
27042 | 612 |
\end{tabular} |
613 |
||
28788 | 614 |
\medskip The Isabelle document preparation system |
615 |
\cite{isabelle-sys} allows tagged command regions to be presented |
|
27042 | 616 |
specifically, e.g.\ to fold proof texts, or drop parts of the text |
617 |
completely. |
|
618 |
||
40406 | 619 |
For example ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{25}{\isacharpercent}}invisible\ auto{\isaliteral{22}{\isachardoublequote}}}'' causes |
28788 | 620 |
that piece of proof to be treated as \isa{invisible} instead of |
40406 | 621 |
\isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{22}{\isachardoublequote}}} (the default), which may be shown or hidden |
622 |
depending on the document setup. In contrast, ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{25}{\isacharpercent}}visible\ auto{\isaliteral{22}{\isachardoublequote}}}'' forces this text to be shown |
|
27042 | 623 |
invariably. |
624 |
||
625 |
Explicit tag specifications within a proof apply to all subsequent |
|
40406 | 626 |
commands of the same level of nesting. For example, ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{25}{\isacharpercent}}visible\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}'' forces the whole |
28788 | 627 |
sub-proof to be typeset as \isa{visible} (unless some of its parts |
628 |
are tagged differently). |
|
629 |
||
630 |
\medskip Command tags merely produce certain markup environments for |
|
631 |
type-setting. The meaning of these is determined by {\LaTeX} |
|
40802 | 632 |
macros, as defined in \verb|~~/lib/texinputs/isabelle.sty| or |
28788 | 633 |
by the document author. The Isabelle document preparation tools |
634 |
also provide some high-level options to specify the meaning of |
|
635 |
arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding |
|
636 |
parts of the text. Logic sessions may also specify ``document |
|
637 |
versions'', where given tags are interpreted in some particular way. |
|
638 |
Again see \cite{isabelle-sys} for further details.% |
|
27042 | 639 |
\end{isamarkuptext}% |
640 |
\isamarkuptrue% |
|
641 |
% |
|
42658 | 642 |
\isamarkupsection{Railroad diagrams% |
643 |
} |
|
644 |
\isamarkuptrue% |
|
645 |
% |
|
646 |
\begin{isamarkuptext}% |
|
647 |
\begin{matharray}{rcl} |
|
648 |
\indexdef{}{antiquotation}{rail}\hypertarget{antiquotation.rail}{\hyperlink{antiquotation.rail}{\mbox{\isa{rail}}}} & : & \isa{antiquotation} \\ |
|
649 |
\end{matharray} |
|
650 |
||
651 |
\begin{railoutput} |
|
42662 | 652 |
\rail@begin{1}{} |
42658 | 653 |
\rail@term{\isa{rail}}[] |
654 |
\rail@nont{\isa{string}}[] |
|
655 |
\rail@end |
|
656 |
\end{railoutput} |
|
657 |
||
658 |
||
659 |
The \hyperlink{antiquotation.rail}{\mbox{\isa{rail}}} antiquotation allows to include syntax |
|
660 |
diagrams into Isabelle documents. {\LaTeX} requires the style file |
|
661 |
\verb|~~/lib/texinputs/pdfsetup.sty|, which can be used via |
|
662 |
\verb|\usepackage{pdfsetup}| in \verb|root.tex|, for |
|
663 |
example. |
|
664 |
||
665 |
The rail specification language is quoted here as Isabelle \hyperlink{syntax.string}{\mbox{\isa{string}}}; it has its own grammar given below. |
|
666 |
||
667 |
\begin{railoutput} |
|
42662 | 668 |
\rail@begin{3}{} |
42658 | 669 |
\rail@plus |
670 |
\rail@bar |
|
671 |
\rail@nextbar{1} |
|
672 |
\rail@nont{\isa{rule}}[] |
|
673 |
\rail@endbar |
|
674 |
\rail@nextplus{2} |
|
675 |
\rail@cterm{\isa{{\isaliteral{3B}{\isacharsemicolon}}}}[] |
|
676 |
\rail@endplus |
|
677 |
\rail@end |
|
678 |
\rail@begin{3}{\isa{rule}} |
|
679 |
\rail@bar |
|
680 |
\rail@nextbar{1} |
|
681 |
\rail@bar |
|
682 |
\rail@nont{\isa{identifier}}[] |
|
683 |
\rail@nextbar{2} |
|
684 |
\rail@nont{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}[] |
|
685 |
\rail@endbar |
|
686 |
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[] |
|
687 |
\rail@endbar |
|
688 |
\rail@nont{\isa{body}}[] |
|
689 |
\rail@end |
|
690 |
\rail@begin{2}{\isa{body}} |
|
691 |
\rail@plus |
|
692 |
\rail@nont{\isa{concatenation}}[] |
|
693 |
\rail@nextplus{1} |
|
694 |
\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[] |
|
695 |
\rail@endplus |
|
696 |
\rail@end |
|
697 |
\rail@begin{3}{\isa{concatenation}} |
|
698 |
\rail@plus |
|
699 |
\rail@nont{\isa{atom}}[] |
|
700 |
\rail@bar |
|
701 |
\rail@nextbar{1} |
|
702 |
\rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[] |
|
703 |
\rail@endbar |
|
704 |
\rail@nextplus{2} |
|
705 |
\rail@endplus |
|
706 |
\rail@bar |
|
707 |
\rail@nextbar{1} |
|
708 |
\rail@bar |
|
709 |
\rail@term{\isa{{\isaliteral{2A}{\isacharasterisk}}}}[] |
|
710 |
\rail@nextbar{2} |
|
711 |
\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[] |
|
712 |
\rail@endbar |
|
713 |
\rail@bar |
|
714 |
\rail@nextbar{2} |
|
715 |
\rail@nont{\isa{atom}}[] |
|
716 |
\rail@endbar |
|
717 |
\rail@endbar |
|
718 |
\rail@end |
|
719 |
\rail@begin{6}{\isa{atom}} |
|
720 |
\rail@bar |
|
721 |
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[] |
|
722 |
\rail@bar |
|
723 |
\rail@nextbar{1} |
|
724 |
\rail@nont{\isa{body}}[] |
|
725 |
\rail@endbar |
|
726 |
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] |
|
727 |
\rail@nextbar{2} |
|
728 |
\rail@nont{\isa{identifier}}[] |
|
729 |
\rail@nextbar{3} |
|
730 |
\rail@bar |
|
731 |
\rail@nextbar{4} |
|
732 |
\rail@term{\isa{{\isaliteral{40}{\isacharat}}}}[] |
|
733 |
\rail@endbar |
|
734 |
\rail@bar |
|
735 |
\rail@nont{\isa{string}}[] |
|
736 |
\rail@nextbar{4} |
|
737 |
\rail@nont{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}[] |
|
738 |
\rail@endbar |
|
739 |
\rail@nextbar{5} |
|
740 |
\rail@term{\isa{{\isaliteral{5C}{\isacharbackslash}}{\isaliteral{5C}{\isacharbackslash}}}}[] |
|
741 |
\rail@endbar |
|
742 |
\rail@end |
|
743 |
\end{railoutput} |
|
744 |
||
745 |
||
746 |
The lexical syntax of \isa{{\isaliteral{22}{\isachardoublequote}}identifier{\isaliteral{22}{\isachardoublequote}}} coincides with that of |
|
747 |
\hyperlink{syntax.ident}{\mbox{\isa{ident}}} in regular Isabelle syntax, but \isa{string} uses |
|
748 |
single quotes instead of double quotes of the standard \hyperlink{syntax.string}{\mbox{\isa{string}}} category, to avoid extra escapes. |
|
749 |
||
750 |
Each \isa{rule} defines a formal language (with optional name), |
|
751 |
using a notation that is similar to EBNF or regular expressions with |
|
752 |
recursion. The meaning and visual appearance of these rail language |
|
753 |
elements is illustrated by the following representative examples. |
|
754 |
||
755 |
\begin{itemize} |
|
756 |
||
757 |
\item Empty \verb|()| |
|
758 |
||
759 |
\begin{railoutput} |
|
42662 | 760 |
\rail@begin{1}{} |
42658 | 761 |
\rail@end |
762 |
\end{railoutput} |
|
763 |
||
764 |
||
765 |
\item Nonterminal \verb|A| |
|
766 |
||
767 |
\begin{railoutput} |
|
42662 | 768 |
\rail@begin{1}{} |
42658 | 769 |
\rail@nont{\isa{A}}[] |
770 |
\rail@end |
|
771 |
\end{railoutput} |
|
772 |
||
773 |
||
774 |
\item Nonterminal via Isabelle antiquotation |
|
775 |
\verb|@{syntax method}| |
|
776 |
||
777 |
\begin{railoutput} |
|
42662 | 778 |
\rail@begin{1}{} |
42658 | 779 |
\rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[] |
780 |
\rail@end |
|
781 |
\end{railoutput} |
|
782 |
||
783 |
||
784 |
\item Terminal \verb|'xyz'| |
|
785 |
||
786 |
\begin{railoutput} |
|
42662 | 787 |
\rail@begin{1}{} |
42658 | 788 |
\rail@term{\isa{xyz}}[] |
789 |
\rail@end |
|
790 |
\end{railoutput} |
|
791 |
||
792 |
||
793 |
\item Terminal in keyword style \verb|@'xyz'| |
|
794 |
||
795 |
\begin{railoutput} |
|
42662 | 796 |
\rail@begin{1}{} |
42658 | 797 |
\rail@term{\isa{\isakeyword{xyz}}}[] |
798 |
\rail@end |
|
799 |
\end{railoutput} |
|
800 |
||
801 |
||
802 |
\item Terminal via Isabelle antiquotation |
|
803 |
\verb|@@{method rule}| |
|
804 |
||
805 |
\begin{railoutput} |
|
42662 | 806 |
\rail@begin{1}{} |
42658 | 807 |
\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[] |
808 |
\rail@end |
|
809 |
\end{railoutput} |
|
810 |
||
811 |
||
812 |
\item Concatenation \verb|A B C| |
|
813 |
||
814 |
\begin{railoutput} |
|
42662 | 815 |
\rail@begin{1}{} |
42658 | 816 |
\rail@nont{\isa{A}}[] |
817 |
\rail@nont{\isa{B}}[] |
|
818 |
\rail@nont{\isa{C}}[] |
|
819 |
\rail@end |
|
820 |
\end{railoutput} |
|
821 |
||
822 |
||
823 |
\item Linebreak \verb|\\| inside |
|
824 |
concatenation\footnote{Strictly speaking, this is only a single |
|
825 |
backslash, but the enclosing \hyperlink{syntax.string}{\mbox{\isa{string}}} syntax requires a |
|
826 |
second one for escaping.} \verb|A B C \\ D E F| |
|
827 |
||
828 |
\begin{railoutput} |
|
42662 | 829 |
\rail@begin{3}{} |
42658 | 830 |
\rail@nont{\isa{A}}[] |
831 |
\rail@nont{\isa{B}}[] |
|
832 |
\rail@nont{\isa{C}}[] |
|
833 |
\rail@cr{2} |
|
834 |
\rail@nont{\isa{D}}[] |
|
835 |
\rail@nont{\isa{E}}[] |
|
836 |
\rail@nont{\isa{F}}[] |
|
837 |
\rail@end |
|
838 |
\end{railoutput} |
|
839 |
||
840 |
||
841 |
\item Variants \verb|A |\verb,|,\verb| B |\verb,|,\verb| C| |
|
842 |
||
843 |
\begin{railoutput} |
|
42662 | 844 |
\rail@begin{3}{} |
42658 | 845 |
\rail@bar |
846 |
\rail@nont{\isa{A}}[] |
|
847 |
\rail@nextbar{1} |
|
848 |
\rail@nont{\isa{B}}[] |
|
849 |
\rail@nextbar{2} |
|
850 |
\rail@nont{\isa{C}}[] |
|
851 |
\rail@endbar |
|
852 |
\rail@end |
|
853 |
\end{railoutput} |
|
854 |
||
855 |
||
856 |
\item Option \verb|A ?| |
|
857 |
||
858 |
\begin{railoutput} |
|
42662 | 859 |
\rail@begin{2}{} |
42658 | 860 |
\rail@bar |
861 |
\rail@nextbar{1} |
|
862 |
\rail@nont{\isa{A}}[] |
|
863 |
\rail@endbar |
|
864 |
\rail@end |
|
865 |
\end{railoutput} |
|
866 |
||
867 |
||
868 |
\item Repetition \verb|A *| |
|
869 |
||
870 |
\begin{railoutput} |
|
42662 | 871 |
\rail@begin{2}{} |
42658 | 872 |
\rail@plus |
873 |
\rail@nextplus{1} |
|
874 |
\rail@cnont{\isa{A}}[] |
|
875 |
\rail@endplus |
|
876 |
\rail@end |
|
877 |
\end{railoutput} |
|
878 |
||
879 |
||
880 |
\item Repetition with separator \verb|A * sep| |
|
881 |
||
882 |
\begin{railoutput} |
|
42662 | 883 |
\rail@begin{3}{} |
42658 | 884 |
\rail@bar |
885 |
\rail@nextbar{1} |
|
886 |
\rail@plus |
|
887 |
\rail@nont{\isa{A}}[] |
|
888 |
\rail@nextplus{2} |
|
889 |
\rail@cnont{\isa{sep}}[] |
|
890 |
\rail@endplus |
|
891 |
\rail@endbar |
|
892 |
\rail@end |
|
893 |
\end{railoutput} |
|
894 |
||
895 |
||
896 |
\item Strict repetition \verb|A +| |
|
897 |
||
898 |
\begin{railoutput} |
|
42662 | 899 |
\rail@begin{2}{} |
42658 | 900 |
\rail@plus |
901 |
\rail@nont{\isa{A}}[] |
|
902 |
\rail@nextplus{1} |
|
903 |
\rail@endplus |
|
904 |
\rail@end |
|
905 |
\end{railoutput} |
|
906 |
||
907 |
||
908 |
\item Strict repetition with separator \verb|A + sep| |
|
909 |
||
910 |
\begin{railoutput} |
|
42662 | 911 |
\rail@begin{2}{} |
42658 | 912 |
\rail@plus |
913 |
\rail@nont{\isa{A}}[] |
|
914 |
\rail@nextplus{1} |
|
915 |
\rail@cnont{\isa{sep}}[] |
|
916 |
\rail@endplus |
|
917 |
\rail@end |
|
918 |
\end{railoutput} |
|
919 |
||
920 |
||
921 |
\end{itemize}% |
|
922 |
\end{isamarkuptext}% |
|
923 |
\isamarkuptrue% |
|
924 |
% |
|
27042 | 925 |
\isamarkupsection{Draft presentation% |
926 |
} |
|
927 |
\isamarkuptrue% |
|
928 |
% |
|
929 |
\begin{isamarkuptext}% |
|
930 |
\begin{matharray}{rcl} |
|
40406 | 931 |
\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}}} \\ |
932 |
\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}}} \\ |
|
27042 | 933 |
\end{matharray} |
934 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
935 |
\begin{railoutput} |
42662 | 936 |
\rail@begin{2}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
937 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
938 |
\rail@term{\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isaliteral{5F}{\isacharunderscore}}drafts}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
939 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
940 |
\rail@term{\hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}drafts}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
941 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
942 |
\rail@plus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
943 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
944 |
\rail@nextplus{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
945 |
\rail@endplus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
946 |
\rail@end |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
947 |
\end{railoutput} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40879
diff
changeset
|
948 |
|
27042 | 949 |
|
28788 | 950 |
\begin{description} |
27042 | 951 |
|
40406 | 952 |
\item \hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isaliteral{5F}{\isacharunderscore}}drafts}}}}~\isa{paths} and \hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}drafts}}}}~\isa{paths} perform simple output of a given list |
27042 | 953 |
of raw source files. Only those symbols that do not require |
954 |
additional {\LaTeX} packages are displayed properly, everything else |
|
955 |
is left verbatim. |
|
956 |
||
28788 | 957 |
\end{description}% |
27042 | 958 |
\end{isamarkuptext}% |
959 |
\isamarkuptrue% |
|
960 |
% |
|
961 |
\isadelimtheory |
|
962 |
% |
|
963 |
\endisadelimtheory |
|
964 |
% |
|
965 |
\isatagtheory |
|
966 |
\isacommand{end}\isamarkupfalse% |
|
967 |
% |
|
968 |
\endisatagtheory |
|
969 |
{\isafoldtheory}% |
|
970 |
% |
|
971 |
\isadelimtheory |
|
972 |
% |
|
973 |
\endisadelimtheory |
|
974 |
\isanewline |
|
975 |
\end{isabellebody}% |
|
976 |
%%% Local Variables: |
|
977 |
%%% mode: latex |
|
978 |
%%% TeX-master: "root" |
|
979 |
%%% End: |