1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sun May 01 18:57:45 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon May 02 01:05:50 2011 +0200
1.3 @@ -31,17 +31,47 @@
1.4 \indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
1.5 \end{matharray}
1.6
1.7 - \begin{rail}
1.8 - 'typedef' altname? abstype '=' repset
1.9 - ;
1.10 + \begin{railoutput}
1.11 +\rail@begin{2}{\isa{}}
1.12 +\rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[]
1.13 +\rail@bar
1.14 +\rail@nextbar{1}
1.15 +\rail@nont{\isa{altname}}[]
1.16 +\rail@endbar
1.17 +\rail@nont{\isa{abstype}}[]
1.18 +\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.19 +\rail@nont{\isa{repset}}[]
1.20 +\rail@end
1.21 +\rail@begin{3}{\isa{altname}}
1.22 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.23 +\rail@bar
1.24 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.25 +\rail@nextbar{1}
1.26 +\rail@term{\isa{\isakeyword{open}}}[]
1.27 +\rail@nextbar{2}
1.28 +\rail@term{\isa{\isakeyword{open}}}[]
1.29 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.30 +\rail@endbar
1.31 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.32 +\rail@end
1.33 +\rail@begin{2}{\isa{abstype}}
1.34 +\rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
1.35 +\rail@bar
1.36 +\rail@nextbar{1}
1.37 +\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
1.38 +\rail@endbar
1.39 +\rail@end
1.40 +\rail@begin{2}{\isa{repset}}
1.41 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.42 +\rail@bar
1.43 +\rail@nextbar{1}
1.44 +\rail@term{\isa{\isakeyword{morphisms}}}[]
1.45 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.46 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.47 +\rail@endbar
1.48 +\rail@end
1.49 +\end{railoutput}
1.50
1.51 - altname: '(' (name | 'open' | 'open' name) ')'
1.52 - ;
1.53 - abstype: typespecsorts mixfix?
1.54 - ;
1.55 - repset: term ('morphisms' name name)?
1.56 - ;
1.57 - \end{rail}
1.58
1.59 \begin{description}
1.60
1.61 @@ -89,13 +119,21 @@
1.62 %
1.63 \begin{isamarkuptext}%
1.64 \begin{matharray}{rcl}
1.65 - \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{attribute} \\
1.66 + \indexdef{HOL}{attribute}{split\_format}\hypertarget{attribute.HOL.split-format}{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{attribute} \\
1.67 \end{matharray}
1.68
1.69 - \begin{rail}
1.70 - 'split_format' '(' 'complete' ')'
1.71 - ;
1.72 - \end{rail}
1.73 + \begin{railoutput}
1.74 +\rail@begin{2}{\isa{}}
1.75 +\rail@term{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
1.76 +\rail@bar
1.77 +\rail@nextbar{1}
1.78 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.79 +\rail@term{\isa{complete}}[]
1.80 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.81 +\rail@endbar
1.82 +\rail@end
1.83 +\end{railoutput}
1.84 +
1.85
1.86 \begin{description}
1.87
1.88 @@ -198,10 +236,23 @@
1.89 \indexdef{HOL}{command}{record}\hypertarget{command.HOL.record}{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
1.90 \end{matharray}
1.91
1.92 - \begin{rail}
1.93 - 'record' typespecsorts '=' (type '+')? (constdecl +)
1.94 - ;
1.95 - \end{rail}
1.96 + \begin{railoutput}
1.97 +\rail@begin{2}{\isa{}}
1.98 +\rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]
1.99 +\rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
1.100 +\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.101 +\rail@bar
1.102 +\rail@nextbar{1}
1.103 +\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
1.104 +\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
1.105 +\rail@endbar
1.106 +\rail@plus
1.107 +\rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
1.108 +\rail@nextplus{1}
1.109 +\rail@endplus
1.110 +\rail@end
1.111 +\end{railoutput}
1.112 +
1.113
1.114 \begin{description}
1.115
1.116 @@ -358,16 +409,61 @@
1.117 \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep-datatype}{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
1.118 \end{matharray}
1.119
1.120 - \begin{rail}
1.121 - 'datatype' (dtspec + 'and')
1.122 - ;
1.123 - 'rep_datatype' ('(' (name +) ')')? (term +)
1.124 - ;
1.125 + \begin{railoutput}
1.126 +\rail@begin{2}{\isa{}}
1.127 +\rail@term{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
1.128 +\rail@plus
1.129 +\rail@nont{\isa{dtspec}}[]
1.130 +\rail@nextplus{1}
1.131 +\rail@cterm{\isa{\isakeyword{and}}}[]
1.132 +\rail@endplus
1.133 +\rail@end
1.134 +\rail@begin{3}{\isa{}}
1.135 +\rail@term{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
1.136 +\rail@bar
1.137 +\rail@nextbar{1}
1.138 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.139 +\rail@plus
1.140 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.141 +\rail@nextplus{2}
1.142 +\rail@endplus
1.143 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.144 +\rail@endbar
1.145 +\rail@plus
1.146 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.147 +\rail@nextplus{1}
1.148 +\rail@endplus
1.149 +\rail@end
1.150 +\rail@begin{2}{\isa{dtspec}}
1.151 +\rail@bar
1.152 +\rail@nextbar{1}
1.153 +\rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]
1.154 +\rail@endbar
1.155 +\rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
1.156 +\rail@bar
1.157 +\rail@nextbar{1}
1.158 +\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
1.159 +\rail@endbar
1.160 +\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.161 +\rail@plus
1.162 +\rail@nont{\isa{cons}}[]
1.163 +\rail@nextplus{1}
1.164 +\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.165 +\rail@endplus
1.166 +\rail@end
1.167 +\rail@begin{2}{\isa{cons}}
1.168 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.169 +\rail@plus
1.170 +\rail@nextplus{1}
1.171 +\rail@cnont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
1.172 +\rail@endplus
1.173 +\rail@bar
1.174 +\rail@nextbar{1}
1.175 +\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
1.176 +\rail@endbar
1.177 +\rail@end
1.178 +\end{railoutput}
1.179
1.180 - dtspec: parname? typespec mixfix? '=' (cons + '|')
1.181 - ;
1.182 - cons: name ( type * ) mixfix?
1.183 - \end{rail}
1.184
1.185 \begin{description}
1.186
1.187 @@ -402,10 +498,18 @@
1.188 \indexdef{HOL}{command}{enriched\_type}\hypertarget{command.HOL.enriched-type}{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
1.189 \end{matharray}
1.190
1.191 - \begin{rail}
1.192 - 'enriched_type' (prefix ':')? term
1.193 - ;
1.194 - \end{rail}
1.195 + \begin{railoutput}
1.196 +\rail@begin{2}{\isa{}}
1.197 +\rail@term{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
1.198 +\rail@bar
1.199 +\rail@nextbar{1}
1.200 +\rail@nont{\isa{prefix}}[]
1.201 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1.202 +\rail@endbar
1.203 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.204 +\rail@end
1.205 +\end{railoutput}
1.206 + % FIXME check prefix
1.207
1.208 \begin{description}
1.209
1.210 @@ -447,17 +551,69 @@
1.211 \indexdef{HOL}{command}{termination}\hypertarget{command.HOL.termination}{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
1.212 \end{matharray}
1.213
1.214 - \begin{rail}
1.215 - 'primrec' target? fixes 'where' equations
1.216 - ;
1.217 - ('fun' | 'function') target? functionopts? fixes \\ 'where' equations
1.218 - ;
1.219 - equations: (thmdecl? prop + '|')
1.220 - ;
1.221 - functionopts: '(' (('sequential' | 'domintros') + ',') ')'
1.222 - ;
1.223 - 'termination' ( term )?
1.224 - \end{rail}
1.225 + \begin{railoutput}
1.226 +\rail@begin{2}{\isa{}}
1.227 +\rail@term{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
1.228 +\rail@bar
1.229 +\rail@nextbar{1}
1.230 +\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.231 +\rail@endbar
1.232 +\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.233 +\rail@term{\isa{\isakeyword{where}}}[]
1.234 +\rail@nont{\isa{equations}}[]
1.235 +\rail@end
1.236 +\rail@begin{4}{\isa{}}
1.237 +\rail@bar
1.238 +\rail@term{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}}[]
1.239 +\rail@nextbar{1}
1.240 +\rail@term{\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}}[]
1.241 +\rail@endbar
1.242 +\rail@bar
1.243 +\rail@nextbar{1}
1.244 +\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.245 +\rail@endbar
1.246 +\rail@bar
1.247 +\rail@nextbar{1}
1.248 +\rail@nont{\isa{functionopts}}[]
1.249 +\rail@endbar
1.250 +\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.251 +\rail@cr{3}
1.252 +\rail@term{\isa{\isakeyword{where}}}[]
1.253 +\rail@nont{\isa{equations}}[]
1.254 +\rail@end
1.255 +\rail@begin{3}{\isa{equations}}
1.256 +\rail@plus
1.257 +\rail@bar
1.258 +\rail@nextbar{1}
1.259 +\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.260 +\rail@endbar
1.261 +\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.262 +\rail@nextplus{2}
1.263 +\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.264 +\rail@endplus
1.265 +\rail@end
1.266 +\rail@begin{3}{\isa{functionopts}}
1.267 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.268 +\rail@plus
1.269 +\rail@bar
1.270 +\rail@term{\isa{sequential}}[]
1.271 +\rail@nextbar{1}
1.272 +\rail@term{\isa{domintros}}[]
1.273 +\rail@endbar
1.274 +\rail@nextplus{2}
1.275 +\rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
1.276 +\rail@endplus
1.277 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.278 +\rail@end
1.279 +\rail@begin{2}{\isa{}}
1.280 +\rail@term{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}}[]
1.281 +\rail@bar
1.282 +\rail@nextbar{1}
1.283 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.284 +\rail@endbar
1.285 +\rail@end
1.286 +\end{railoutput}
1.287 +
1.288
1.289 \begin{description}
1.290
1.291 @@ -539,15 +695,40 @@
1.292 \indexdef{HOL}{method}{size\_change}\hypertarget{method.HOL.size-change}{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}} & : & \isa{method} \\
1.293 \end{matharray}
1.294
1.295 - \begin{rail}
1.296 - 'relation' term
1.297 - ;
1.298 - 'lexicographic_order' ( clasimpmod * )
1.299 - ;
1.300 - 'size_change' ( orders ( clasimpmod * ) )
1.301 - ;
1.302 - orders: ( 'max' | 'min' | 'ms' ) *
1.303 - \end{rail}
1.304 + \begin{railoutput}
1.305 +\rail@begin{1}{\isa{}}
1.306 +\rail@term{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}}[]
1.307 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.308 +\rail@end
1.309 +\rail@begin{2}{\isa{}}
1.310 +\rail@term{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}}[]
1.311 +\rail@plus
1.312 +\rail@nextplus{1}
1.313 +\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1.314 +\rail@endplus
1.315 +\rail@end
1.316 +\rail@begin{2}{\isa{}}
1.317 +\rail@term{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}}[]
1.318 +\rail@nont{\isa{orders}}[]
1.319 +\rail@plus
1.320 +\rail@nextplus{1}
1.321 +\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1.322 +\rail@endplus
1.323 +\rail@end
1.324 +\rail@begin{4}{\isa{orders}}
1.325 +\rail@plus
1.326 +\rail@nextplus{1}
1.327 +\rail@bar
1.328 +\rail@term{\isa{max}}[]
1.329 +\rail@nextbar{2}
1.330 +\rail@term{\isa{min}}[]
1.331 +\rail@nextbar{3}
1.332 +\rail@term{\isa{ms}}[]
1.333 +\rail@endbar
1.334 +\rail@endplus
1.335 +\rail@end
1.336 +\end{railoutput}
1.337 +
1.338
1.339 \begin{description}
1.340
1.341 @@ -599,9 +780,27 @@
1.342 \indexdef{HOL}{attribute}{partial\_function\_mono}\hypertarget{attribute.HOL.partial-function-mono}{\hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}}} & : & \isa{attribute} \\
1.343 \end{matharray}
1.344
1.345 - \begin{rail}
1.346 - 'partial_function' target? '(' mode ')' fixes \\ 'where' thmdecl? prop
1.347 - \end{rail}
1.348 + \begin{railoutput}
1.349 +\rail@begin{5}{\isa{}}
1.350 +\rail@term{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}}[]
1.351 +\rail@bar
1.352 +\rail@nextbar{1}
1.353 +\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.354 +\rail@endbar
1.355 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.356 +\rail@nont{\isa{mode}}[]
1.357 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.358 +\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.359 +\rail@cr{3}
1.360 +\rail@term{\isa{\isakeyword{where}}}[]
1.361 +\rail@bar
1.362 +\rail@nextbar{4}
1.363 +\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.364 +\rail@endbar
1.365 +\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.366 +\rail@end
1.367 +\end{railoutput}
1.368 + % FIXME check mode
1.369
1.370 \begin{description}
1.371
1.372 @@ -666,18 +865,76 @@
1.373 \indexdef{HOL}{command}{recdef\_tc}\hypertarget{command.HOL.recdef-tc}{\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
1.374 \end{matharray}
1.375
1.376 - \begin{rail}
1.377 - 'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
1.378 - ;
1.379 - recdeftc thmdecl? tc
1.380 - ;
1.381 - hints: '(' 'hints' ( recdefmod * ) ')'
1.382 - ;
1.383 - recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
1.384 - ;
1.385 - tc: nameref ('(' nat ')')?
1.386 - ;
1.387 - \end{rail}
1.388 + \begin{railoutput}
1.389 +\rail@begin{5}{\isa{}}
1.390 +\rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[]
1.391 +\rail@bar
1.392 +\rail@nextbar{1}
1.393 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.394 +\rail@term{\isa{\isakeyword{permissive}}}[]
1.395 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.396 +\rail@endbar
1.397 +\rail@cr{3}
1.398 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.399 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.400 +\rail@plus
1.401 +\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.402 +\rail@nextplus{4}
1.403 +\rail@endplus
1.404 +\rail@bar
1.405 +\rail@nextbar{4}
1.406 +\rail@nont{\isa{hints}}[]
1.407 +\rail@endbar
1.408 +\rail@end
1.409 +\rail@begin{2}{\isa{}}
1.410 +\rail@nont{\isa{recdeftc}}[]
1.411 +\rail@bar
1.412 +\rail@nextbar{1}
1.413 +\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.414 +\rail@endbar
1.415 +\rail@nont{\isa{tc}}[]
1.416 +\rail@end
1.417 +\rail@begin{2}{\isa{hints}}
1.418 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.419 +\rail@term{\isa{\isakeyword{hints}}}[]
1.420 +\rail@plus
1.421 +\rail@nextplus{1}
1.422 +\rail@cnont{\isa{recdefmod}}[]
1.423 +\rail@endplus
1.424 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.425 +\rail@end
1.426 +\rail@begin{4}{\isa{recdefmod}}
1.427 +\rail@bar
1.428 +\rail@bar
1.429 +\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}[]
1.430 +\rail@nextbar{1}
1.431 +\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}[]
1.432 +\rail@nextbar{2}
1.433 +\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}[]
1.434 +\rail@endbar
1.435 +\rail@bar
1.436 +\rail@nextbar{1}
1.437 +\rail@term{\isa{add}}[]
1.438 +\rail@nextbar{2}
1.439 +\rail@term{\isa{del}}[]
1.440 +\rail@endbar
1.441 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1.442 +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.443 +\rail@nextbar{3}
1.444 +\rail@nont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1.445 +\rail@endbar
1.446 +\rail@end
1.447 +\rail@begin{2}{\isa{tc}}
1.448 +\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
1.449 +\rail@bar
1.450 +\rail@nextbar{1}
1.451 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.452 +\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1.453 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.454 +\rail@endbar
1.455 +\rail@end
1.456 +\end{railoutput}
1.457 +
1.458
1.459 \begin{description}
1.460
1.461 @@ -710,10 +967,23 @@
1.462 \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef-wf}{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}}} & : & \isa{attribute} \\
1.463 \end{matharray}
1.464
1.465 - \begin{rail}
1.466 - ('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del')
1.467 - ;
1.468 - \end{rail}%
1.469 + \begin{railoutput}
1.470 +\rail@begin{3}{\isa{}}
1.471 +\rail@bar
1.472 +\rail@term{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}}[]
1.473 +\rail@nextbar{1}
1.474 +\rail@term{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}}}[]
1.475 +\rail@nextbar{2}
1.476 +\rail@term{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}}}[]
1.477 +\rail@endbar
1.478 +\rail@bar
1.479 +\rail@nextbar{1}
1.480 +\rail@term{\isa{add}}[]
1.481 +\rail@nextbar{2}
1.482 +\rail@term{\isa{del}}[]
1.483 +\rail@endbar
1.484 +\rail@end
1.485 +\end{railoutput}%
1.486 \end{isamarkuptext}%
1.487 \isamarkuptrue%
1.488 %
1.489 @@ -752,15 +1022,61 @@
1.490 \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isa{attribute} \\
1.491 \end{matharray}
1.492
1.493 - \begin{rail}
1.494 - ('inductive' | 'inductive_set' | 'coinductive' | 'coinductive_set') target? fixes ('for' fixes)? \\
1.495 - ('where' clauses)? ('monos' thmrefs)?
1.496 - ;
1.497 - clauses: (thmdecl? prop + '|')
1.498 - ;
1.499 - 'mono' (() | 'add' | 'del')
1.500 - ;
1.501 - \end{rail}
1.502 + \begin{railoutput}
1.503 +\rail@begin{7}{\isa{}}
1.504 +\rail@bar
1.505 +\rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
1.506 +\rail@nextbar{1}
1.507 +\rail@term{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}}}[]
1.508 +\rail@nextbar{2}
1.509 +\rail@term{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}}[]
1.510 +\rail@nextbar{3}
1.511 +\rail@term{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}}}[]
1.512 +\rail@endbar
1.513 +\rail@bar
1.514 +\rail@nextbar{1}
1.515 +\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.516 +\rail@endbar
1.517 +\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.518 +\rail@bar
1.519 +\rail@nextbar{1}
1.520 +\rail@term{\isa{\isakeyword{for}}}[]
1.521 +\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.522 +\rail@endbar
1.523 +\rail@cr{5}
1.524 +\rail@bar
1.525 +\rail@nextbar{6}
1.526 +\rail@term{\isa{\isakeyword{where}}}[]
1.527 +\rail@nont{\isa{clauses}}[]
1.528 +\rail@endbar
1.529 +\rail@bar
1.530 +\rail@nextbar{6}
1.531 +\rail@term{\isa{\isakeyword{monos}}}[]
1.532 +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.533 +\rail@endbar
1.534 +\rail@end
1.535 +\rail@begin{3}{\isa{clauses}}
1.536 +\rail@plus
1.537 +\rail@bar
1.538 +\rail@nextbar{1}
1.539 +\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.540 +\rail@endbar
1.541 +\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.542 +\rail@nextplus{2}
1.543 +\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.544 +\rail@endplus
1.545 +\rail@end
1.546 +\rail@begin{3}{\isa{}}
1.547 +\rail@term{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}}[]
1.548 +\rail@bar
1.549 +\rail@nextbar{1}
1.550 +\rail@term{\isa{add}}[]
1.551 +\rail@nextbar{2}
1.552 +\rail@term{\isa{del}}[]
1.553 +\rail@endbar
1.554 +\rail@end
1.555 +\end{railoutput}
1.556 +
1.557
1.558 \begin{description}
1.559
1.560 @@ -893,10 +1209,16 @@
1.561 \indexdef{HOL}{method}{iprover}\hypertarget{method.HOL.iprover}{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\
1.562 \end{matharray}
1.563
1.564 - \begin{rail}
1.565 - 'iprover' ( rulemod * )
1.566 - ;
1.567 - \end{rail}
1.568 + \begin{railoutput}
1.569 +\rail@begin{2}{\isa{}}
1.570 +\rail@term{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}}[]
1.571 +\rail@plus
1.572 +\rail@nextplus{1}
1.573 +\rail@cnont{\hyperlink{syntax.rulemod}{\mbox{\isa{rulemod}}}}[]
1.574 +\rail@endplus
1.575 +\rail@end
1.576 +\end{railoutput}
1.577 +
1.578
1.579 The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof
1.580 search, depending on specifically declared rules from the context,
1.581 @@ -923,10 +1245,16 @@
1.582 \indexdef{HOL}{method}{coherent}\hypertarget{method.HOL.coherent}{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}} & : & \isa{method} \\
1.583 \end{matharray}
1.584
1.585 - \begin{rail}
1.586 - 'coherent' thmrefs?
1.587 - ;
1.588 - \end{rail}
1.589 + \begin{railoutput}
1.590 +\rail@begin{2}{\isa{}}
1.591 +\rail@term{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}}[]
1.592 +\rail@bar
1.593 +\rail@nextbar{1}
1.594 +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.595 +\rail@endbar
1.596 +\rail@end
1.597 +\end{railoutput}
1.598 +
1.599
1.600 The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of
1.601 \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
1.602 @@ -952,25 +1280,89 @@
1.603 \indexdef{HOL}{command}{sledgehammer\_params}\hypertarget{command.HOL.sledgehammer-params}{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
1.604 \end{matharray}
1.605
1.606 - \begin{rail}
1.607 - 'solve_direct'
1.608 - ;
1.609 -
1.610 - 'try' ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' thmrefs ) + ) ? nat?
1.611 - ;
1.612 -
1.613 - 'sledgehammer' ( '[' args ']' ) ? facts? nat?
1.614 - ;
1.615 -
1.616 - 'sledgehammer_params' ( ( '[' args ']' ) ? )
1.617 - ;
1.618 -
1.619 - args: ( name '=' value + ',' )
1.620 - ;
1.621 -
1.622 - facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? thmrefs ) + ) ? ')'
1.623 - ;
1.624 - \end{rail}
1.625 + \begin{railoutput}
1.626 +\rail@begin{6}{\isa{}}
1.627 +\rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[]
1.628 +\rail@bar
1.629 +\rail@nextbar{1}
1.630 +\rail@plus
1.631 +\rail@bar
1.632 +\rail@term{\isa{simp}}[]
1.633 +\rail@nextbar{2}
1.634 +\rail@term{\isa{intro}}[]
1.635 +\rail@nextbar{3}
1.636 +\rail@term{\isa{elim}}[]
1.637 +\rail@nextbar{4}
1.638 +\rail@term{\isa{dest}}[]
1.639 +\rail@endbar
1.640 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1.641 +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.642 +\rail@nextplus{5}
1.643 +\rail@endplus
1.644 +\rail@endbar
1.645 +\rail@bar
1.646 +\rail@nextbar{1}
1.647 +\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1.648 +\rail@endbar
1.649 +\rail@end
1.650 +\rail@begin{2}{\isa{}}
1.651 +\rail@term{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}[]
1.652 +\rail@bar
1.653 +\rail@nextbar{1}
1.654 +\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
1.655 +\rail@nont{\isa{args}}[]
1.656 +\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
1.657 +\rail@endbar
1.658 +\rail@bar
1.659 +\rail@nextbar{1}
1.660 +\rail@nont{\isa{facts}}[]
1.661 +\rail@endbar
1.662 +\rail@bar
1.663 +\rail@nextbar{1}
1.664 +\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1.665 +\rail@endbar
1.666 +\rail@end
1.667 +\rail@begin{2}{\isa{}}
1.668 +\rail@term{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
1.669 +\rail@bar
1.670 +\rail@nextbar{1}
1.671 +\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
1.672 +\rail@nont{\isa{args}}[]
1.673 +\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
1.674 +\rail@endbar
1.675 +\rail@end
1.676 +\rail@begin{2}{\isa{args}}
1.677 +\rail@plus
1.678 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.679 +\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.680 +\rail@nont{\isa{value}}[]
1.681 +\rail@nextplus{1}
1.682 +\rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
1.683 +\rail@endplus
1.684 +\rail@end
1.685 +\rail@begin{5}{\isa{facts}}
1.686 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.687 +\rail@bar
1.688 +\rail@nextbar{1}
1.689 +\rail@plus
1.690 +\rail@bar
1.691 +\rail@nextbar{2}
1.692 +\rail@bar
1.693 +\rail@term{\isa{add}}[]
1.694 +\rail@nextbar{3}
1.695 +\rail@term{\isa{del}}[]
1.696 +\rail@endbar
1.697 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1.698 +\rail@endbar
1.699 +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.700 +\rail@nextplus{4}
1.701 +\rail@endplus
1.702 +\rail@endbar
1.703 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.704 +\rail@end
1.705 +\end{railoutput}
1.706 + % FIXME try: proper clasimpmod!?
1.707 + % FIXME check args "value"
1.708
1.709 \begin{description}
1.710
1.711 @@ -1014,22 +1406,74 @@
1.712 \indexdef{HOL}{command}{nitpick\_params}\hypertarget{command.HOL.nitpick-params}{\hyperlink{command.HOL.nitpick-params}{\mbox{\isa{\isacommand{nitpick{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
1.713 \end{matharray}
1.714
1.715 - \begin{rail}
1.716 - 'value' ( ( '[' name ']' ) ? ) modes? term
1.717 - ;
1.718 -
1.719 - ('quickcheck' | 'refute' | 'nitpick') ( ( '[' args ']' ) ? ) nat?
1.720 - ;
1.721 -
1.722 - ('quickcheck_params' | 'refute_params' | 'nitpick_params') ( ( '[' args ']' ) ? )
1.723 - ;
1.724 -
1.725 - modes: '(' (name + ) ')'
1.726 - ;
1.727 -
1.728 - args: ( name '=' value + ',' )
1.729 - ;
1.730 - \end{rail}
1.731 + \begin{railoutput}
1.732 +\rail@begin{2}{\isa{}}
1.733 +\rail@term{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}[]
1.734 +\rail@bar
1.735 +\rail@nextbar{1}
1.736 +\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
1.737 +\rail@nont{\isa{name}}[]
1.738 +\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
1.739 +\rail@endbar
1.740 +\rail@bar
1.741 +\rail@nextbar{1}
1.742 +\rail@nont{\isa{modes}}[]
1.743 +\rail@endbar
1.744 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.745 +\rail@end
1.746 +\rail@begin{3}{\isa{}}
1.747 +\rail@bar
1.748 +\rail@term{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}[]
1.749 +\rail@nextbar{1}
1.750 +\rail@term{\hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}}}[]
1.751 +\rail@nextbar{2}
1.752 +\rail@term{\hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}}}[]
1.753 +\rail@endbar
1.754 +\rail@bar
1.755 +\rail@nextbar{1}
1.756 +\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
1.757 +\rail@nont{\isa{args}}[]
1.758 +\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
1.759 +\rail@endbar
1.760 +\rail@bar
1.761 +\rail@nextbar{1}
1.762 +\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1.763 +\rail@endbar
1.764 +\rail@end
1.765 +\rail@begin{3}{\isa{}}
1.766 +\rail@bar
1.767 +\rail@term{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
1.768 +\rail@nextbar{1}
1.769 +\rail@term{\hyperlink{command.HOL.refute-params}{\mbox{\isa{\isacommand{refute{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
1.770 +\rail@nextbar{2}
1.771 +\rail@term{\hyperlink{command.HOL.nitpick-params}{\mbox{\isa{\isacommand{nitpick{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
1.772 +\rail@endbar
1.773 +\rail@bar
1.774 +\rail@nextbar{1}
1.775 +\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
1.776 +\rail@nont{\isa{args}}[]
1.777 +\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
1.778 +\rail@endbar
1.779 +\rail@end
1.780 +\rail@begin{2}{\isa{modes}}
1.781 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.782 +\rail@plus
1.783 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.784 +\rail@nextplus{1}
1.785 +\rail@endplus
1.786 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.787 +\rail@end
1.788 +\rail@begin{2}{\isa{args}}
1.789 +\rail@plus
1.790 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.791 +\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.792 +\rail@nont{\isa{value}}[]
1.793 +\rail@nextplus{1}
1.794 +\rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
1.795 +\rail@endplus
1.796 +\rail@end
1.797 +\end{railoutput}
1.798 + % FIXME check "value"
1.799
1.800 \begin{description}
1.801
1.802 @@ -1154,19 +1598,75 @@
1.803 \indexdef{HOL}{command}{inductive\_cases}\hypertarget{command.HOL.inductive-cases}{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
1.804 \end{matharray}
1.805
1.806 - \begin{rail}
1.807 - 'case_tac' goalspec? term rule?
1.808 - ;
1.809 - 'induct_tac' goalspec? (insts * 'and') rule?
1.810 - ;
1.811 - 'ind_cases' (prop +) ('for' (name +)) ?
1.812 - ;
1.813 - 'inductive_cases' (thmdecl? (prop +) + 'and')
1.814 - ;
1.815 + \begin{railoutput}
1.816 +\rail@begin{2}{\isa{}}
1.817 +\rail@term{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
1.818 +\rail@bar
1.819 +\rail@nextbar{1}
1.820 +\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
1.821 +\rail@endbar
1.822 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.823 +\rail@bar
1.824 +\rail@nextbar{1}
1.825 +\rail@nont{\isa{rule}}[]
1.826 +\rail@endbar
1.827 +\rail@end
1.828 +\rail@begin{3}{\isa{}}
1.829 +\rail@term{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
1.830 +\rail@bar
1.831 +\rail@nextbar{1}
1.832 +\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
1.833 +\rail@endbar
1.834 +\rail@bar
1.835 +\rail@nextbar{1}
1.836 +\rail@plus
1.837 +\rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
1.838 +\rail@nextplus{2}
1.839 +\rail@cterm{\isa{\isakeyword{and}}}[]
1.840 +\rail@endplus
1.841 +\rail@endbar
1.842 +\rail@bar
1.843 +\rail@nextbar{1}
1.844 +\rail@nont{\isa{rule}}[]
1.845 +\rail@endbar
1.846 +\rail@end
1.847 +\rail@begin{3}{\isa{}}
1.848 +\rail@term{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}[]
1.849 +\rail@plus
1.850 +\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.851 +\rail@nextplus{1}
1.852 +\rail@endplus
1.853 +\rail@bar
1.854 +\rail@nextbar{1}
1.855 +\rail@term{\isa{\isakeyword{for}}}[]
1.856 +\rail@plus
1.857 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.858 +\rail@nextplus{2}
1.859 +\rail@endplus
1.860 +\rail@endbar
1.861 +\rail@end
1.862 +\rail@begin{3}{\isa{}}
1.863 +\rail@term{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[]
1.864 +\rail@plus
1.865 +\rail@bar
1.866 +\rail@nextbar{1}
1.867 +\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.868 +\rail@endbar
1.869 +\rail@plus
1.870 +\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.871 +\rail@nextplus{1}
1.872 +\rail@endplus
1.873 +\rail@nextplus{2}
1.874 +\rail@cterm{\isa{\isakeyword{and}}}[]
1.875 +\rail@endplus
1.876 +\rail@end
1.877 +\rail@begin{1}{\isa{rule}}
1.878 +\rail@term{\isa{rule}}[]
1.879 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1.880 +\rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
1.881 +\rail@end
1.882 +\end{railoutput}
1.883
1.884 - rule: ('rule' ':' thmref)
1.885 - ;
1.886 - \end{rail}
1.887
1.888 \begin{description}
1.889
1.890 @@ -1237,85 +1737,317 @@
1.891 \indexdef{HOL}{command}{code\_reflect}\hypertarget{command.HOL.code-reflect}{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
1.892 \end{matharray}
1.893
1.894 - \begin{rail}
1.895 - 'export_code' ( constexpr + ) \\
1.896 - ( ( 'in' target ( 'module_name' string ) ? \\
1.897 - ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
1.898 - ;
1.899 + \begin{railoutput}
1.900 +\rail@begin{11}{\isa{}}
1.901 +\rail@term{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
1.902 +\rail@plus
1.903 +\rail@nont{\isa{constexpr}}[]
1.904 +\rail@nextplus{1}
1.905 +\rail@endplus
1.906 +\rail@cr{3}
1.907 +\rail@bar
1.908 +\rail@nextbar{4}
1.909 +\rail@plus
1.910 +\rail@term{\isa{\isakeyword{in}}}[]
1.911 +\rail@nont{\isa{target}}[]
1.912 +\rail@bar
1.913 +\rail@nextbar{5}
1.914 +\rail@term{\isa{\isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}}}[]
1.915 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.916 +\rail@endbar
1.917 +\rail@cr{7}
1.918 +\rail@bar
1.919 +\rail@nextbar{8}
1.920 +\rail@term{\isa{\isakeyword{file}}}[]
1.921 +\rail@bar
1.922 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.923 +\rail@nextbar{9}
1.924 +\rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
1.925 +\rail@endbar
1.926 +\rail@endbar
1.927 +\rail@bar
1.928 +\rail@nextbar{8}
1.929 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.930 +\rail@nont{\isa{args}}[]
1.931 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.932 +\rail@endbar
1.933 +\rail@nextplus{10}
1.934 +\rail@endplus
1.935 +\rail@endbar
1.936 +\rail@end
1.937 +\rail@begin{1}{\isa{const}}
1.938 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.939 +\rail@end
1.940 +\rail@begin{3}{\isa{constexpr}}
1.941 +\rail@bar
1.942 +\rail@nont{\isa{const}}[]
1.943 +\rail@nextbar{1}
1.944 +\rail@term{\isa{name{\isaliteral{2E}{\isachardot}}{\isaliteral{5F}{\isacharunderscore}}}}[]
1.945 +\rail@nextbar{2}
1.946 +\rail@term{\isa{{\isaliteral{5F}{\isacharunderscore}}}}[]
1.947 +\rail@endbar
1.948 +\rail@end
1.949 +\rail@begin{1}{\isa{typeconstructor}}
1.950 +\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
1.951 +\rail@end
1.952 +\rail@begin{1}{\isa{class}}
1.953 +\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
1.954 +\rail@end
1.955 +\rail@begin{4}{\isa{target}}
1.956 +\rail@bar
1.957 +\rail@term{\isa{SML}}[]
1.958 +\rail@nextbar{1}
1.959 +\rail@term{\isa{OCaml}}[]
1.960 +\rail@nextbar{2}
1.961 +\rail@term{\isa{Haskell}}[]
1.962 +\rail@nextbar{3}
1.963 +\rail@term{\isa{Scala}}[]
1.964 +\rail@endbar
1.965 +\rail@end
1.966 +\rail@begin{4}{\isa{}}
1.967 +\rail@term{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}}[]
1.968 +\rail@bar
1.969 +\rail@nextbar{1}
1.970 +\rail@bar
1.971 +\rail@term{\isa{del}}[]
1.972 +\rail@nextbar{2}
1.973 +\rail@term{\isa{abstype}}[]
1.974 +\rail@nextbar{3}
1.975 +\rail@term{\isa{abstract}}[]
1.976 +\rail@endbar
1.977 +\rail@endbar
1.978 +\rail@end
1.979 +\rail@begin{2}{\isa{}}
1.980 +\rail@term{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}}}[]
1.981 +\rail@plus
1.982 +\rail@nont{\isa{const}}[]
1.983 +\rail@nextplus{1}
1.984 +\rail@endplus
1.985 +\rail@end
1.986 +\rail@begin{2}{\isa{}}
1.987 +\rail@term{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
1.988 +\rail@plus
1.989 +\rail@nont{\isa{const}}[]
1.990 +\rail@nextplus{1}
1.991 +\rail@endplus
1.992 +\rail@end
1.993 +\rail@begin{2}{\isa{}}
1.994 +\rail@term{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}}}[]
1.995 +\rail@bar
1.996 +\rail@nextbar{1}
1.997 +\rail@term{\isa{del}}[]
1.998 +\rail@endbar
1.999 +\rail@end
1.1000 +\rail@begin{2}{\isa{}}
1.1001 +\rail@term{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}}}[]
1.1002 +\rail@bar
1.1003 +\rail@nextbar{1}
1.1004 +\rail@term{\isa{del}}[]
1.1005 +\rail@endbar
1.1006 +\rail@end
1.1007 +\rail@begin{3}{\isa{}}
1.1008 +\rail@term{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[]
1.1009 +\rail@bar
1.1010 +\rail@nextbar{1}
1.1011 +\rail@plus
1.1012 +\rail@nont{\isa{constexpr}}[]
1.1013 +\rail@nextplus{2}
1.1014 +\rail@endplus
1.1015 +\rail@endbar
1.1016 +\rail@end
1.1017 +\rail@begin{3}{\isa{}}
1.1018 +\rail@term{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
1.1019 +\rail@bar
1.1020 +\rail@nextbar{1}
1.1021 +\rail@plus
1.1022 +\rail@nont{\isa{constexpr}}[]
1.1023 +\rail@nextplus{2}
1.1024 +\rail@endplus
1.1025 +\rail@endbar
1.1026 +\rail@end
1.1027 +\rail@begin{7}{\isa{}}
1.1028 +\rail@term{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}}}[]
1.1029 +\rail@plus
1.1030 +\rail@nont{\isa{const}}[]
1.1031 +\rail@nextplus{1}
1.1032 +\rail@cterm{\isa{\isakeyword{and}}}[]
1.1033 +\rail@endplus
1.1034 +\rail@cr{3}
1.1035 +\rail@plus
1.1036 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1037 +\rail@nont{\isa{target}}[]
1.1038 +\rail@plus
1.1039 +\rail@bar
1.1040 +\rail@nextbar{4}
1.1041 +\rail@nont{\isa{syntax}}[]
1.1042 +\rail@endbar
1.1043 +\rail@nextplus{5}
1.1044 +\rail@cterm{\isa{\isakeyword{and}}}[]
1.1045 +\rail@endplus
1.1046 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1047 +\rail@nextplus{6}
1.1048 +\rail@endplus
1.1049 +\rail@end
1.1050 +\rail@begin{7}{\isa{}}
1.1051 +\rail@term{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
1.1052 +\rail@plus
1.1053 +\rail@nont{\isa{typeconstructor}}[]
1.1054 +\rail@nextplus{1}
1.1055 +\rail@cterm{\isa{\isakeyword{and}}}[]
1.1056 +\rail@endplus
1.1057 +\rail@cr{3}
1.1058 +\rail@plus
1.1059 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1060 +\rail@nont{\isa{target}}[]
1.1061 +\rail@plus
1.1062 +\rail@bar
1.1063 +\rail@nextbar{4}
1.1064 +\rail@nont{\isa{syntax}}[]
1.1065 +\rail@endbar
1.1066 +\rail@nextplus{5}
1.1067 +\rail@cterm{\isa{\isakeyword{and}}}[]
1.1068 +\rail@endplus
1.1069 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1070 +\rail@nextplus{6}
1.1071 +\rail@endplus
1.1072 +\rail@end
1.1073 +\rail@begin{9}{\isa{}}
1.1074 +\rail@term{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}}}[]
1.1075 +\rail@plus
1.1076 +\rail@nont{\isa{class}}[]
1.1077 +\rail@nextplus{1}
1.1078 +\rail@cterm{\isa{\isakeyword{and}}}[]
1.1079 +\rail@endplus
1.1080 +\rail@cr{3}
1.1081 +\rail@plus
1.1082 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1083 +\rail@nont{\isa{target}}[]
1.1084 +\rail@cr{5}
1.1085 +\rail@plus
1.1086 +\rail@bar
1.1087 +\rail@nextbar{6}
1.1088 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.1089 +\rail@endbar
1.1090 +\rail@nextplus{7}
1.1091 +\rail@cterm{\isa{\isakeyword{and}}}[]
1.1092 +\rail@endplus
1.1093 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1094 +\rail@nextplus{8}
1.1095 +\rail@endplus
1.1096 +\rail@end
1.1097 +\rail@begin{7}{\isa{}}
1.1098 +\rail@term{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}}}[]
1.1099 +\rail@plus
1.1100 +\rail@nont{\isa{typeconstructor}}[]
1.1101 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
1.1102 +\rail@nont{\isa{class}}[]
1.1103 +\rail@nextplus{1}
1.1104 +\rail@cterm{\isa{\isakeyword{and}}}[]
1.1105 +\rail@endplus
1.1106 +\rail@cr{3}
1.1107 +\rail@plus
1.1108 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1109 +\rail@nont{\isa{target}}[]
1.1110 +\rail@plus
1.1111 +\rail@bar
1.1112 +\rail@nextbar{4}
1.1113 +\rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
1.1114 +\rail@endbar
1.1115 +\rail@nextplus{5}
1.1116 +\rail@cterm{\isa{\isakeyword{and}}}[]
1.1117 +\rail@endplus
1.1118 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1119 +\rail@nextplus{6}
1.1120 +\rail@endplus
1.1121 +\rail@end
1.1122 +\rail@begin{2}{\isa{}}
1.1123 +\rail@term{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}}}[]
1.1124 +\rail@nont{\isa{target}}[]
1.1125 +\rail@plus
1.1126 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.1127 +\rail@nextplus{1}
1.1128 +\rail@endplus
1.1129 +\rail@end
1.1130 +\rail@begin{1}{\isa{}}
1.1131 +\rail@term{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}}}[]
1.1132 +\rail@nont{\isa{const}}[]
1.1133 +\rail@nont{\isa{const}}[]
1.1134 +\rail@nont{\isa{target}}[]
1.1135 +\rail@end
1.1136 +\rail@begin{2}{\isa{}}
1.1137 +\rail@term{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}}}[]
1.1138 +\rail@nont{\isa{target}}[]
1.1139 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.1140 +\rail@bar
1.1141 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.1142 +\rail@nextbar{1}
1.1143 +\rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
1.1144 +\rail@endbar
1.1145 +\rail@end
1.1146 +\rail@begin{2}{\isa{}}
1.1147 +\rail@term{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}}}[]
1.1148 +\rail@nont{\isa{target}}[]
1.1149 +\rail@plus
1.1150 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.1151 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.1152 +\rail@nextplus{1}
1.1153 +\rail@endplus
1.1154 +\rail@end
1.1155 +\rail@begin{11}{\isa{}}
1.1156 +\rail@term{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}}[]
1.1157 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.1158 +\rail@cr{2}
1.1159 +\rail@bar
1.1160 +\rail@nextbar{3}
1.1161 +\rail@term{\isa{\isakeyword{datatypes}}}[]
1.1162 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.1163 +\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.1164 +\rail@bar
1.1165 +\rail@term{\isa{{\isaliteral{5F}{\isacharunderscore}}}}[]
1.1166 +\rail@nextbar{4}
1.1167 +\rail@plus
1.1168 +\rail@plus
1.1169 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.1170 +\rail@nextplus{5}
1.1171 +\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.1172 +\rail@endplus
1.1173 +\rail@nextplus{6}
1.1174 +\rail@cterm{\isa{\isakeyword{and}}}[]
1.1175 +\rail@endplus
1.1176 +\rail@endbar
1.1177 +\rail@endbar
1.1178 +\rail@cr{8}
1.1179 +\rail@bar
1.1180 +\rail@nextbar{9}
1.1181 +\rail@term{\isa{\isakeyword{functions}}}[]
1.1182 +\rail@plus
1.1183 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.1184 +\rail@nextplus{10}
1.1185 +\rail@endplus
1.1186 +\rail@endbar
1.1187 +\rail@bar
1.1188 +\rail@nextbar{9}
1.1189 +\rail@term{\isa{\isakeyword{file}}}[]
1.1190 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.1191 +\rail@endbar
1.1192 +\rail@end
1.1193 +\rail@begin{4}{\isa{syntax}}
1.1194 +\rail@bar
1.1195 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.1196 +\rail@nextbar{1}
1.1197 +\rail@bar
1.1198 +\rail@term{\isa{\isakeyword{infix}}}[]
1.1199 +\rail@nextbar{2}
1.1200 +\rail@term{\isa{\isakeyword{infixl}}}[]
1.1201 +\rail@nextbar{3}
1.1202 +\rail@term{\isa{\isakeyword{infixr}}}[]
1.1203 +\rail@endbar
1.1204 +\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1.1205 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.1206 +\rail@endbar
1.1207 +\rail@end
1.1208 +\end{railoutput}
1.1209
1.1210 - const: term
1.1211 - ;
1.1212 -
1.1213 - constexpr: ( const | 'name._' | '_' )
1.1214 - ;
1.1215 -
1.1216 - typeconstructor: nameref
1.1217 - ;
1.1218 -
1.1219 - class: nameref
1.1220 - ;
1.1221 -
1.1222 - target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'
1.1223 - ;
1.1224 -
1.1225 - 'code' ( 'del' | 'abstype' | 'abstract' ) ?
1.1226 - ;
1.1227 -
1.1228 - 'code_abort' ( const + )
1.1229 - ;
1.1230 -
1.1231 - 'code_datatype' ( const + )
1.1232 - ;
1.1233 -
1.1234 - 'code_inline' ( 'del' ) ?
1.1235 - ;
1.1236 -
1.1237 - 'code_post' ( 'del' ) ?
1.1238 - ;
1.1239 -
1.1240 - 'code_thms' ( constexpr + ) ?
1.1241 - ;
1.1242 -
1.1243 - 'code_deps' ( constexpr + ) ?
1.1244 - ;
1.1245 -
1.1246 - 'code_const' (const + 'and') \\
1.1247 - ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
1.1248 - ;
1.1249 -
1.1250 - 'code_type' (typeconstructor + 'and') \\
1.1251 - ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
1.1252 - ;
1.1253 -
1.1254 - 'code_class' (class + 'and') \\
1.1255 - ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
1.1256 - ;
1.1257 -
1.1258 - 'code_instance' (( typeconstructor '::' class ) + 'and') \\
1.1259 - ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
1.1260 - ;
1.1261 -
1.1262 - 'code_reserved' target ( string + )
1.1263 - ;
1.1264 -
1.1265 - 'code_monad' const const target
1.1266 - ;
1.1267 -
1.1268 - 'code_include' target ( string ( string | '-') )
1.1269 - ;
1.1270 -
1.1271 - 'code_modulename' target ( ( string string ) + )
1.1272 - ;
1.1273 -
1.1274 - 'code_reflect' string \\
1.1275 - ( 'datatypes' ( string '=' ( '_' | ( string + '|' ) + 'and' ) ) ) ? \\
1.1276 - ( 'functions' ( string + ) ) ? ( 'file' string ) ?
1.1277 - ;
1.1278 -
1.1279 - syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
1.1280 - ;
1.1281 -
1.1282 - \end{rail}
1.1283
1.1284 \begin{description}
1.1285
1.1286 @@ -1438,39 +2170,115 @@
1.1287 \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
1.1288 \end{matharray}
1.1289
1.1290 - \begin{rail}
1.1291 - ( 'code_module' | 'code_library' ) modespec ? name ? \\
1.1292 - ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
1.1293 - 'contains' ( ( name '=' term ) + | term + )
1.1294 - ;
1.1295 -
1.1296 - modespec: '(' ( name * ) ')'
1.1297 - ;
1.1298 -
1.1299 - 'consts_code' (codespec +)
1.1300 - ;
1.1301 -
1.1302 - codespec: const template attachment ?
1.1303 - ;
1.1304 -
1.1305 - 'types_code' (tycodespec +)
1.1306 - ;
1.1307 -
1.1308 - tycodespec: name template attachment ?
1.1309 - ;
1.1310 -
1.1311 - const: term
1.1312 - ;
1.1313 -
1.1314 - template: '(' string ')'
1.1315 - ;
1.1316 -
1.1317 - attachment: 'attach' modespec ? verblbrace text verbrbrace
1.1318 - ;
1.1319 -
1.1320 - 'code' (name)?
1.1321 - ;
1.1322 - \end{rail}%
1.1323 + \begin{railoutput}
1.1324 +\rail@begin{11}{\isa{}}
1.1325 +\rail@bar
1.1326 +\rail@term{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}}[]
1.1327 +\rail@nextbar{1}
1.1328 +\rail@term{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}}[]
1.1329 +\rail@endbar
1.1330 +\rail@bar
1.1331 +\rail@nextbar{1}
1.1332 +\rail@nont{\isa{modespec}}[]
1.1333 +\rail@endbar
1.1334 +\rail@bar
1.1335 +\rail@nextbar{1}
1.1336 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1337 +\rail@endbar
1.1338 +\rail@cr{3}
1.1339 +\rail@bar
1.1340 +\rail@nextbar{4}
1.1341 +\rail@term{\isa{\isakeyword{file}}}[]
1.1342 +\rail@nont{\isa{name}}[]
1.1343 +\rail@endbar
1.1344 +\rail@bar
1.1345 +\rail@nextbar{4}
1.1346 +\rail@term{\isa{\isakeyword{imports}}}[]
1.1347 +\rail@plus
1.1348 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1349 +\rail@nextplus{5}
1.1350 +\rail@endplus
1.1351 +\rail@endbar
1.1352 +\rail@cr{7}
1.1353 +\rail@term{\isa{\isakeyword{contains}}}[]
1.1354 +\rail@bar
1.1355 +\rail@plus
1.1356 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1357 +\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.1358 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.1359 +\rail@nextplus{8}
1.1360 +\rail@endplus
1.1361 +\rail@nextbar{9}
1.1362 +\rail@plus
1.1363 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.1364 +\rail@nextplus{10}
1.1365 +\rail@endplus
1.1366 +\rail@endbar
1.1367 +\rail@end
1.1368 +\rail@begin{2}{\isa{modespec}}
1.1369 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1370 +\rail@plus
1.1371 +\rail@nextplus{1}
1.1372 +\rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1373 +\rail@endplus
1.1374 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1375 +\rail@end
1.1376 +\rail@begin{2}{\isa{}}
1.1377 +\rail@term{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
1.1378 +\rail@plus
1.1379 +\rail@nont{\isa{codespec}}[]
1.1380 +\rail@nextplus{1}
1.1381 +\rail@endplus
1.1382 +\rail@end
1.1383 +\rail@begin{2}{\isa{codespec}}
1.1384 +\rail@nont{\isa{const}}[]
1.1385 +\rail@nont{\isa{template}}[]
1.1386 +\rail@bar
1.1387 +\rail@nextbar{1}
1.1388 +\rail@nont{\isa{attachment}}[]
1.1389 +\rail@endbar
1.1390 +\rail@end
1.1391 +\rail@begin{2}{\isa{}}
1.1392 +\rail@term{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
1.1393 +\rail@plus
1.1394 +\rail@nont{\isa{tycodespec}}[]
1.1395 +\rail@nextplus{1}
1.1396 +\rail@endplus
1.1397 +\rail@end
1.1398 +\rail@begin{2}{\isa{tycodespec}}
1.1399 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1400 +\rail@nont{\isa{template}}[]
1.1401 +\rail@bar
1.1402 +\rail@nextbar{1}
1.1403 +\rail@nont{\isa{attachment}}[]
1.1404 +\rail@endbar
1.1405 +\rail@end
1.1406 +\rail@begin{1}{\isa{const}}
1.1407 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.1408 +\rail@end
1.1409 +\rail@begin{1}{\isa{template}}
1.1410 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1411 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1.1412 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1413 +\rail@end
1.1414 +\rail@begin{2}{\isa{attachment}}
1.1415 +\rail@term{\isa{attach}}[]
1.1416 +\rail@bar
1.1417 +\rail@nextbar{1}
1.1418 +\rail@nont{\isa{modespec}}[]
1.1419 +\rail@endbar
1.1420 +\rail@term{\isa{{\isaliteral{7B}{\isacharbraceleft}}}}[]
1.1421 +\rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
1.1422 +\rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
1.1423 +\rail@end
1.1424 +\rail@begin{2}{\isa{}}
1.1425 +\rail@term{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}}[]
1.1426 +\rail@bar
1.1427 +\rail@nextbar{1}
1.1428 +\rail@nont{\isa{name}}[]
1.1429 +\rail@endbar
1.1430 +\rail@end
1.1431 +\end{railoutput}%
1.1432 \end{isamarkuptext}%
1.1433 \isamarkuptrue%
1.1434 %
1.1435 @@ -1484,11 +2292,45 @@
1.1436 \indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax-specification}{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
1.1437 \end{matharray}
1.1438
1.1439 - \begin{rail}
1.1440 - ('specification' | 'ax_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
1.1441 - ;
1.1442 - decl: ((name ':')? term '(' 'overloaded' ')'?)
1.1443 - \end{rail}
1.1444 + \begin{railoutput}
1.1445 +\rail@begin{6}{\isa{}}
1.1446 +\rail@bar
1.1447 +\rail@term{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}}[]
1.1448 +\rail@nextbar{1}
1.1449 +\rail@term{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}}}[]
1.1450 +\rail@endbar
1.1451 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1452 +\rail@plus
1.1453 +\rail@nont{\isa{decl}}[]
1.1454 +\rail@nextplus{1}
1.1455 +\rail@endplus
1.1456 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1457 +\rail@cr{3}
1.1458 +\rail@plus
1.1459 +\rail@bar
1.1460 +\rail@nextbar{4}
1.1461 +\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.1462 +\rail@endbar
1.1463 +\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.1464 +\rail@nextplus{5}
1.1465 +\rail@endplus
1.1466 +\rail@end
1.1467 +\rail@begin{2}{\isa{decl}}
1.1468 +\rail@bar
1.1469 +\rail@nextbar{1}
1.1470 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1471 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1.1472 +\rail@endbar
1.1473 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.1474 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1475 +\rail@term{\isa{\isakeyword{overloaded}}}[]
1.1476 +\rail@bar
1.1477 +\rail@nextbar{1}
1.1478 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1479 +\rail@endbar
1.1480 +\rail@end
1.1481 +\end{railoutput}
1.1482 +
1.1483
1.1484 \begin{description}
1.1485