1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue May 03 20:59:24 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue May 03 21:07:24 2011 +0200
1.3 @@ -32,7 +32,7 @@
1.4 \end{matharray}
1.5
1.6 \begin{railoutput}
1.7 -\rail@begin{2}{\isa{}}
1.8 +\rail@begin{2}{}
1.9 \rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[]
1.10 \rail@bar
1.11 \rail@nextbar{1}
1.12 @@ -123,7 +123,7 @@
1.13 \end{matharray}
1.14
1.15 \begin{railoutput}
1.16 -\rail@begin{2}{\isa{}}
1.17 +\rail@begin{2}{}
1.18 \rail@term{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
1.19 \rail@bar
1.20 \rail@nextbar{1}
1.21 @@ -237,7 +237,7 @@
1.22 \end{matharray}
1.23
1.24 \begin{railoutput}
1.25 -\rail@begin{2}{\isa{}}
1.26 +\rail@begin{2}{}
1.27 \rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]
1.28 \rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
1.29 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.30 @@ -410,7 +410,7 @@
1.31 \end{matharray}
1.32
1.33 \begin{railoutput}
1.34 -\rail@begin{2}{\isa{}}
1.35 +\rail@begin{2}{}
1.36 \rail@term{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
1.37 \rail@plus
1.38 \rail@nont{\isa{dtspec}}[]
1.39 @@ -418,7 +418,7 @@
1.40 \rail@cterm{\isa{\isakeyword{and}}}[]
1.41 \rail@endplus
1.42 \rail@end
1.43 -\rail@begin{3}{\isa{}}
1.44 +\rail@begin{3}{}
1.45 \rail@term{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
1.46 \rail@bar
1.47 \rail@nextbar{1}
1.48 @@ -499,7 +499,7 @@
1.49 \end{matharray}
1.50
1.51 \begin{railoutput}
1.52 -\rail@begin{2}{\isa{}}
1.53 +\rail@begin{2}{}
1.54 \rail@term{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
1.55 \rail@bar
1.56 \rail@nextbar{1}
1.57 @@ -552,7 +552,7 @@
1.58 \end{matharray}
1.59
1.60 \begin{railoutput}
1.61 -\rail@begin{2}{\isa{}}
1.62 +\rail@begin{2}{}
1.63 \rail@term{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
1.64 \rail@bar
1.65 \rail@nextbar{1}
1.66 @@ -562,7 +562,7 @@
1.67 \rail@term{\isa{\isakeyword{where}}}[]
1.68 \rail@nont{\isa{equations}}[]
1.69 \rail@end
1.70 -\rail@begin{4}{\isa{}}
1.71 +\rail@begin{4}{}
1.72 \rail@bar
1.73 \rail@term{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}}[]
1.74 \rail@nextbar{1}
1.75 @@ -605,7 +605,7 @@
1.76 \rail@endplus
1.77 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.78 \rail@end
1.79 -\rail@begin{2}{\isa{}}
1.80 +\rail@begin{2}{}
1.81 \rail@term{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}}[]
1.82 \rail@bar
1.83 \rail@nextbar{1}
1.84 @@ -696,18 +696,18 @@
1.85 \end{matharray}
1.86
1.87 \begin{railoutput}
1.88 -\rail@begin{1}{\isa{}}
1.89 +\rail@begin{1}{}
1.90 \rail@term{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}}[]
1.91 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.92 \rail@end
1.93 -\rail@begin{2}{\isa{}}
1.94 +\rail@begin{2}{}
1.95 \rail@term{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}}[]
1.96 \rail@plus
1.97 \rail@nextplus{1}
1.98 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1.99 \rail@endplus
1.100 \rail@end
1.101 -\rail@begin{2}{\isa{}}
1.102 +\rail@begin{2}{}
1.103 \rail@term{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}}[]
1.104 \rail@nont{\isa{orders}}[]
1.105 \rail@plus
1.106 @@ -781,7 +781,7 @@
1.107 \end{matharray}
1.108
1.109 \begin{railoutput}
1.110 -\rail@begin{5}{\isa{}}
1.111 +\rail@begin{5}{}
1.112 \rail@term{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}}[]
1.113 \rail@bar
1.114 \rail@nextbar{1}
1.115 @@ -866,7 +866,7 @@
1.116 \end{matharray}
1.117
1.118 \begin{railoutput}
1.119 -\rail@begin{5}{\isa{}}
1.120 +\rail@begin{5}{}
1.121 \rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[]
1.122 \rail@bar
1.123 \rail@nextbar{1}
1.124 @@ -886,7 +886,7 @@
1.125 \rail@nont{\isa{hints}}[]
1.126 \rail@endbar
1.127 \rail@end
1.128 -\rail@begin{2}{\isa{}}
1.129 +\rail@begin{2}{}
1.130 \rail@nont{\isa{recdeftc}}[]
1.131 \rail@bar
1.132 \rail@nextbar{1}
1.133 @@ -968,7 +968,7 @@
1.134 \end{matharray}
1.135
1.136 \begin{railoutput}
1.137 -\rail@begin{3}{\isa{}}
1.138 +\rail@begin{3}{}
1.139 \rail@bar
1.140 \rail@term{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}}[]
1.141 \rail@nextbar{1}
1.142 @@ -1023,7 +1023,7 @@
1.143 \end{matharray}
1.144
1.145 \begin{railoutput}
1.146 -\rail@begin{7}{\isa{}}
1.147 +\rail@begin{7}{}
1.148 \rail@bar
1.149 \rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
1.150 \rail@nextbar{1}
1.151 @@ -1066,7 +1066,7 @@
1.152 \rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.153 \rail@endplus
1.154 \rail@end
1.155 -\rail@begin{3}{\isa{}}
1.156 +\rail@begin{3}{}
1.157 \rail@term{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}}[]
1.158 \rail@bar
1.159 \rail@nextbar{1}
1.160 @@ -1210,7 +1210,7 @@
1.161 \end{matharray}
1.162
1.163 \begin{railoutput}
1.164 -\rail@begin{2}{\isa{}}
1.165 +\rail@begin{2}{}
1.166 \rail@term{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}}[]
1.167 \rail@plus
1.168 \rail@nextplus{1}
1.169 @@ -1246,7 +1246,7 @@
1.170 \end{matharray}
1.171
1.172 \begin{railoutput}
1.173 -\rail@begin{2}{\isa{}}
1.174 +\rail@begin{2}{}
1.175 \rail@term{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}}[]
1.176 \rail@bar
1.177 \rail@nextbar{1}
1.178 @@ -1281,7 +1281,7 @@
1.179 \end{matharray}
1.180
1.181 \begin{railoutput}
1.182 -\rail@begin{6}{\isa{}}
1.183 +\rail@begin{6}{}
1.184 \rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[]
1.185 \rail@bar
1.186 \rail@nextbar{1}
1.187 @@ -1305,7 +1305,7 @@
1.188 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1.189 \rail@endbar
1.190 \rail@end
1.191 -\rail@begin{2}{\isa{}}
1.192 +\rail@begin{2}{}
1.193 \rail@term{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}[]
1.194 \rail@bar
1.195 \rail@nextbar{1}
1.196 @@ -1322,7 +1322,7 @@
1.197 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1.198 \rail@endbar
1.199 \rail@end
1.200 -\rail@begin{2}{\isa{}}
1.201 +\rail@begin{2}{}
1.202 \rail@term{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
1.203 \rail@bar
1.204 \rail@nextbar{1}
1.205 @@ -1407,7 +1407,7 @@
1.206 \end{matharray}
1.207
1.208 \begin{railoutput}
1.209 -\rail@begin{2}{\isa{}}
1.210 +\rail@begin{2}{}
1.211 \rail@term{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}[]
1.212 \rail@bar
1.213 \rail@nextbar{1}
1.214 @@ -1421,7 +1421,7 @@
1.215 \rail@endbar
1.216 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.217 \rail@end
1.218 -\rail@begin{3}{\isa{}}
1.219 +\rail@begin{3}{}
1.220 \rail@bar
1.221 \rail@term{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}[]
1.222 \rail@nextbar{1}
1.223 @@ -1440,7 +1440,7 @@
1.224 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1.225 \rail@endbar
1.226 \rail@end
1.227 -\rail@begin{3}{\isa{}}
1.228 +\rail@begin{3}{}
1.229 \rail@bar
1.230 \rail@term{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
1.231 \rail@nextbar{1}
1.232 @@ -1599,7 +1599,7 @@
1.233 \end{matharray}
1.234
1.235 \begin{railoutput}
1.236 -\rail@begin{2}{\isa{}}
1.237 +\rail@begin{2}{}
1.238 \rail@term{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
1.239 \rail@bar
1.240 \rail@nextbar{1}
1.241 @@ -1611,7 +1611,7 @@
1.242 \rail@nont{\isa{rule}}[]
1.243 \rail@endbar
1.244 \rail@end
1.245 -\rail@begin{3}{\isa{}}
1.246 +\rail@begin{3}{}
1.247 \rail@term{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
1.248 \rail@bar
1.249 \rail@nextbar{1}
1.250 @@ -1630,7 +1630,7 @@
1.251 \rail@nont{\isa{rule}}[]
1.252 \rail@endbar
1.253 \rail@end
1.254 -\rail@begin{3}{\isa{}}
1.255 +\rail@begin{3}{}
1.256 \rail@term{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}[]
1.257 \rail@plus
1.258 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.259 @@ -1645,7 +1645,7 @@
1.260 \rail@endplus
1.261 \rail@endbar
1.262 \rail@end
1.263 -\rail@begin{3}{\isa{}}
1.264 +\rail@begin{3}{}
1.265 \rail@term{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[]
1.266 \rail@plus
1.267 \rail@bar
1.268 @@ -1751,7 +1751,7 @@
1.269 \end{matharray}
1.270
1.271 \begin{railoutput}
1.272 -\rail@begin{11}{\isa{}}
1.273 +\rail@begin{11}{}
1.274 \rail@term{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
1.275 \rail@plus
1.276 \rail@nont{\isa{constexpr}}[]
1.277 @@ -1817,7 +1817,7 @@
1.278 \rail@term{\isa{Scala}}[]
1.279 \rail@endbar
1.280 \rail@end
1.281 -\rail@begin{4}{\isa{}}
1.282 +\rail@begin{4}{}
1.283 \rail@term{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}}[]
1.284 \rail@bar
1.285 \rail@nextbar{1}
1.286 @@ -1830,35 +1830,35 @@
1.287 \rail@endbar
1.288 \rail@endbar
1.289 \rail@end
1.290 -\rail@begin{2}{\isa{}}
1.291 +\rail@begin{2}{}
1.292 \rail@term{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}}}[]
1.293 \rail@plus
1.294 \rail@nont{\isa{const}}[]
1.295 \rail@nextplus{1}
1.296 \rail@endplus
1.297 \rail@end
1.298 -\rail@begin{2}{\isa{}}
1.299 +\rail@begin{2}{}
1.300 \rail@term{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
1.301 \rail@plus
1.302 \rail@nont{\isa{const}}[]
1.303 \rail@nextplus{1}
1.304 \rail@endplus
1.305 \rail@end
1.306 -\rail@begin{2}{\isa{}}
1.307 +\rail@begin{2}{}
1.308 \rail@term{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}}}[]
1.309 \rail@bar
1.310 \rail@nextbar{1}
1.311 \rail@term{\isa{del}}[]
1.312 \rail@endbar
1.313 \rail@end
1.314 -\rail@begin{2}{\isa{}}
1.315 +\rail@begin{2}{}
1.316 \rail@term{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}}}[]
1.317 \rail@bar
1.318 \rail@nextbar{1}
1.319 \rail@term{\isa{del}}[]
1.320 \rail@endbar
1.321 \rail@end
1.322 -\rail@begin{3}{\isa{}}
1.323 +\rail@begin{3}{}
1.324 \rail@term{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[]
1.325 \rail@bar
1.326 \rail@nextbar{1}
1.327 @@ -1868,7 +1868,7 @@
1.328 \rail@endplus
1.329 \rail@endbar
1.330 \rail@end
1.331 -\rail@begin{3}{\isa{}}
1.332 +\rail@begin{3}{}
1.333 \rail@term{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
1.334 \rail@bar
1.335 \rail@nextbar{1}
1.336 @@ -1878,7 +1878,7 @@
1.337 \rail@endplus
1.338 \rail@endbar
1.339 \rail@end
1.340 -\rail@begin{7}{\isa{}}
1.341 +\rail@begin{7}{}
1.342 \rail@term{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}}}[]
1.343 \rail@plus
1.344 \rail@nont{\isa{const}}[]
1.345 @@ -1901,7 +1901,7 @@
1.346 \rail@nextplus{6}
1.347 \rail@endplus
1.348 \rail@end
1.349 -\rail@begin{7}{\isa{}}
1.350 +\rail@begin{7}{}
1.351 \rail@term{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
1.352 \rail@plus
1.353 \rail@nont{\isa{typeconstructor}}[]
1.354 @@ -1924,7 +1924,7 @@
1.355 \rail@nextplus{6}
1.356 \rail@endplus
1.357 \rail@end
1.358 -\rail@begin{9}{\isa{}}
1.359 +\rail@begin{9}{}
1.360 \rail@term{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}}}[]
1.361 \rail@plus
1.362 \rail@nont{\isa{class}}[]
1.363 @@ -1948,7 +1948,7 @@
1.364 \rail@nextplus{8}
1.365 \rail@endplus
1.366 \rail@end
1.367 -\rail@begin{7}{\isa{}}
1.368 +\rail@begin{7}{}
1.369 \rail@term{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}}}[]
1.370 \rail@plus
1.371 \rail@nont{\isa{typeconstructor}}[]
1.372 @@ -1973,7 +1973,7 @@
1.373 \rail@nextplus{6}
1.374 \rail@endplus
1.375 \rail@end
1.376 -\rail@begin{2}{\isa{}}
1.377 +\rail@begin{2}{}
1.378 \rail@term{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}}}[]
1.379 \rail@nont{\isa{target}}[]
1.380 \rail@plus
1.381 @@ -1981,13 +1981,13 @@
1.382 \rail@nextplus{1}
1.383 \rail@endplus
1.384 \rail@end
1.385 -\rail@begin{1}{\isa{}}
1.386 +\rail@begin{1}{}
1.387 \rail@term{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}}}[]
1.388 \rail@nont{\isa{const}}[]
1.389 \rail@nont{\isa{const}}[]
1.390 \rail@nont{\isa{target}}[]
1.391 \rail@end
1.392 -\rail@begin{2}{\isa{}}
1.393 +\rail@begin{2}{}
1.394 \rail@term{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}}}[]
1.395 \rail@nont{\isa{target}}[]
1.396 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.397 @@ -1997,7 +1997,7 @@
1.398 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
1.399 \rail@endbar
1.400 \rail@end
1.401 -\rail@begin{2}{\isa{}}
1.402 +\rail@begin{2}{}
1.403 \rail@term{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}}}[]
1.404 \rail@nont{\isa{target}}[]
1.405 \rail@plus
1.406 @@ -2006,7 +2006,7 @@
1.407 \rail@nextplus{1}
1.408 \rail@endplus
1.409 \rail@end
1.410 -\rail@begin{11}{\isa{}}
1.411 +\rail@begin{11}{}
1.412 \rail@term{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}}[]
1.413 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.414 \rail@cr{2}
1.415 @@ -2189,7 +2189,7 @@
1.416 \end{matharray}
1.417
1.418 \begin{railoutput}
1.419 -\rail@begin{11}{\isa{}}
1.420 +\rail@begin{11}{}
1.421 \rail@bar
1.422 \rail@term{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}}[]
1.423 \rail@nextbar{1}
1.424 @@ -2241,7 +2241,7 @@
1.425 \rail@endplus
1.426 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.427 \rail@end
1.428 -\rail@begin{2}{\isa{}}
1.429 +\rail@begin{2}{}
1.430 \rail@term{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
1.431 \rail@plus
1.432 \rail@nont{\isa{codespec}}[]
1.433 @@ -2256,7 +2256,7 @@
1.434 \rail@nont{\isa{attachment}}[]
1.435 \rail@endbar
1.436 \rail@end
1.437 -\rail@begin{2}{\isa{}}
1.438 +\rail@begin{2}{}
1.439 \rail@term{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
1.440 \rail@plus
1.441 \rail@nont{\isa{tycodespec}}[]
1.442 @@ -2289,7 +2289,7 @@
1.443 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
1.444 \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
1.445 \rail@end
1.446 -\rail@begin{2}{\isa{}}
1.447 +\rail@begin{2}{}
1.448 \rail@term{\hyperlink{attribute.code}{\mbox{\isa{code}}}}[]
1.449 \rail@bar
1.450 \rail@nextbar{1}
1.451 @@ -2565,7 +2565,7 @@
1.452 \end{matharray}
1.453
1.454 \begin{railoutput}
1.455 -\rail@begin{6}{\isa{}}
1.456 +\rail@begin{6}{}
1.457 \rail@bar
1.458 \rail@term{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}}[]
1.459 \rail@nextbar{1}