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