1.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex Tue May 03 20:59:24 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Tue May 03 21:07:24 2011 +0200
1.3 @@ -75,11 +75,11 @@
1.4 \end{matharray}
1.5
1.6 \begin{railoutput}
1.7 -\rail@begin{1}{\isa{}}
1.8 +\rail@begin{1}{}
1.9 \rail@term{\hyperlink{command.notepad}{\mbox{\isa{\isacommand{notepad}}}}}[]
1.10 \rail@term{\isa{\isakeyword{begin}}}[]
1.11 \rail@end
1.12 -\rail@begin{1}{\isa{}}
1.13 +\rail@begin{1}{}
1.14 \rail@term{\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}}[]
1.15 \rail@end
1.16 \end{railoutput}
1.17 @@ -220,7 +220,7 @@
1.18 exporting some result \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} yields \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}t{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}.
1.19
1.20 \begin{railoutput}
1.21 -\rail@begin{2}{\isa{}}
1.22 +\rail@begin{2}{}
1.23 \rail@term{\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}}[]
1.24 \rail@plus
1.25 \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
1.26 @@ -228,7 +228,7 @@
1.27 \rail@cterm{\isa{\isakeyword{and}}}[]
1.28 \rail@endplus
1.29 \rail@end
1.30 -\rail@begin{2}{\isa{}}
1.31 +\rail@begin{2}{}
1.32 \rail@bar
1.33 \rail@term{\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}}[]
1.34 \rail@nextbar{1}
1.35 @@ -240,7 +240,7 @@
1.36 \rail@cterm{\isa{\isakeyword{and}}}[]
1.37 \rail@endplus
1.38 \rail@end
1.39 -\rail@begin{2}{\isa{}}
1.40 +\rail@begin{2}{}
1.41 \rail@term{\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}}[]
1.42 \rail@plus
1.43 \rail@nont{\isa{def}}[]
1.44 @@ -331,7 +331,7 @@
1.45 input process just after type checking. Also note that \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} does not support polymorphism.
1.46
1.47 \begin{railoutput}
1.48 -\rail@begin{3}{\isa{}}
1.49 +\rail@begin{3}{}
1.50 \rail@term{\hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}}[]
1.51 \rail@plus
1.52 \rail@plus
1.53 @@ -403,7 +403,7 @@
1.54 issuing a follow-up claim.
1.55
1.56 \begin{railoutput}
1.57 -\rail@begin{3}{\isa{}}
1.58 +\rail@begin{3}{}
1.59 \rail@term{\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}}[]
1.60 \rail@plus
1.61 \rail@bar
1.62 @@ -415,7 +415,7 @@
1.63 \rail@cterm{\isa{\isakeyword{and}}}[]
1.64 \rail@endplus
1.65 \rail@end
1.66 -\rail@begin{4}{\isa{}}
1.67 +\rail@begin{4}{}
1.68 \rail@bar
1.69 \rail@term{\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}}[]
1.70 \rail@nextbar{1}
1.71 @@ -538,7 +538,7 @@
1.72 and assumptions, cf.\ \secref{sec:obtain}).
1.73
1.74 \begin{railoutput}
1.75 -\rail@begin{6}{\isa{}}
1.76 +\rail@begin{6}{}
1.77 \rail@bar
1.78 \rail@term{\hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}}[]
1.79 \rail@nextbar{1}
1.80 @@ -562,7 +562,7 @@
1.81 \rail@nont{\isa{longgoal}}[]
1.82 \rail@endbar
1.83 \rail@end
1.84 -\rail@begin{4}{\isa{}}
1.85 +\rail@begin{4}{}
1.86 \rail@bar
1.87 \rail@term{\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}}[]
1.88 \rail@nextbar{1}
1.89 @@ -574,7 +574,7 @@
1.90 \rail@endbar
1.91 \rail@nont{\isa{goal}}[]
1.92 \rail@end
1.93 -\rail@begin{2}{\isa{}}
1.94 +\rail@begin{2}{}
1.95 \rail@term{\hyperlink{command.print-statement}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}}}}}[]
1.96 \rail@bar
1.97 \rail@nextbar{1}
1.98 @@ -849,21 +849,21 @@
1.99 assumption in the very last step.
1.100
1.101 \begin{railoutput}
1.102 -\rail@begin{2}{\isa{}}
1.103 +\rail@begin{2}{}
1.104 \rail@term{\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}}[]
1.105 \rail@bar
1.106 \rail@nextbar{1}
1.107 \rail@nont{\isa{method}}[]
1.108 \rail@endbar
1.109 \rail@end
1.110 -\rail@begin{2}{\isa{}}
1.111 +\rail@begin{2}{}
1.112 \rail@term{\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}}[]
1.113 \rail@bar
1.114 \rail@nextbar{1}
1.115 \rail@nont{\isa{method}}[]
1.116 \rail@endbar
1.117 \rail@end
1.118 -\rail@begin{2}{\isa{}}
1.119 +\rail@begin{2}{}
1.120 \rail@term{\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}}[]
1.121 \rail@nont{\isa{method}}[]
1.122 \rail@bar
1.123 @@ -871,7 +871,7 @@
1.124 \rail@nont{\isa{method}}[]
1.125 \rail@endbar
1.126 \rail@end
1.127 -\rail@begin{3}{\isa{}}
1.128 +\rail@begin{3}{}
1.129 \rail@bar
1.130 \rail@term{\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}}[]
1.131 \rail@nextbar{1}
1.132 @@ -954,14 +954,14 @@
1.133 \end{matharray}
1.134
1.135 \begin{railoutput}
1.136 -\rail@begin{2}{\isa{}}
1.137 +\rail@begin{2}{}
1.138 \rail@term{\hyperlink{method.fact}{\mbox{\isa{fact}}}}[]
1.139 \rail@bar
1.140 \rail@nextbar{1}
1.141 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.142 \rail@endbar
1.143 \rail@end
1.144 -\rail@begin{2}{\isa{}}
1.145 +\rail@begin{2}{}
1.146 \rail@term{\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}}[]
1.147 \rail@bar
1.148 \rail@nextbar{1}
1.149 @@ -993,7 +993,7 @@
1.150 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1.151 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.152 \rail@end
1.153 -\rail@begin{3}{\isa{}}
1.154 +\rail@begin{3}{}
1.155 \rail@bar
1.156 \rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[]
1.157 \rail@nextbar{1}
1.158 @@ -1012,15 +1012,15 @@
1.159 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1.160 \rail@endbar
1.161 \rail@end
1.162 -\rail@begin{1}{\isa{}}
1.163 +\rail@begin{1}{}
1.164 \rail@term{\hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}}[]
1.165 \rail@term{\isa{del}}[]
1.166 \rail@end
1.167 -\rail@begin{1}{\isa{}}
1.168 +\rail@begin{1}{}
1.169 \rail@term{\hyperlink{attribute.OF}{\mbox{\isa{OF}}}}[]
1.170 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.171 \rail@end
1.172 -\rail@begin{2}{\isa{}}
1.173 +\rail@begin{2}{}
1.174 \rail@term{\hyperlink{attribute.of}{\mbox{\isa{of}}}}[]
1.175 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
1.176 \rail@bar
1.177 @@ -1030,7 +1030,7 @@
1.178 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
1.179 \rail@endbar
1.180 \rail@end
1.181 -\rail@begin{6}{\isa{}}
1.182 +\rail@begin{6}{}
1.183 \rail@term{\hyperlink{attribute.where}{\mbox{\isa{where}}}}[]
1.184 \rail@bar
1.185 \rail@nextbar{1}
1.186 @@ -1160,7 +1160,7 @@
1.187 \end{matharray}
1.188
1.189 \begin{railoutput}
1.190 -\rail@begin{2}{\isa{}}
1.191 +\rail@begin{2}{}
1.192 \rail@bar
1.193 \rail@term{\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}}[]
1.194 \rail@nextbar{1}
1.195 @@ -1168,14 +1168,14 @@
1.196 \rail@endbar
1.197 \rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
1.198 \rail@end
1.199 -\rail@begin{2}{\isa{}}
1.200 +\rail@begin{2}{}
1.201 \rail@term{\hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}}}[]
1.202 \rail@bar
1.203 \rail@nextbar{1}
1.204 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1.205 \rail@endbar
1.206 \rail@end
1.207 -\rail@begin{1}{\isa{}}
1.208 +\rail@begin{1}{}
1.209 \rail@term{\hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}}[]
1.210 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1.211 \rail@end
1.212 @@ -1234,7 +1234,7 @@
1.213 \end{matharray}
1.214
1.215 \begin{railoutput}
1.216 -\rail@begin{1}{\isa{}}
1.217 +\rail@begin{1}{}
1.218 \rail@term{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
1.219 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.220 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.221 @@ -1309,7 +1309,7 @@
1.222 occur in the conclusion.
1.223
1.224 \begin{railoutput}
1.225 -\rail@begin{2}{\isa{}}
1.226 +\rail@begin{2}{}
1.227 \rail@term{\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}}[]
1.228 \rail@bar
1.229 \rail@nextbar{1}
1.230 @@ -1327,7 +1327,7 @@
1.231 \rail@cterm{\isa{\isakeyword{and}}}[]
1.232 \rail@endplus
1.233 \rail@end
1.234 -\rail@begin{2}{\isa{}}
1.235 +\rail@begin{2}{}
1.236 \rail@term{\hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}}[]
1.237 \rail@plus
1.238 \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
1.239 @@ -1441,7 +1441,7 @@
1.240 \end{matharray}
1.241
1.242 \begin{railoutput}
1.243 -\rail@begin{2}{\isa{}}
1.244 +\rail@begin{2}{}
1.245 \rail@bar
1.246 \rail@term{\hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}}[]
1.247 \rail@nextbar{1}
1.248 @@ -1454,7 +1454,7 @@
1.249 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.250 \rail@endbar
1.251 \rail@end
1.252 -\rail@begin{3}{\isa{}}
1.253 +\rail@begin{3}{}
1.254 \rail@term{\hyperlink{attribute.trans}{\mbox{\isa{trans}}}}[]
1.255 \rail@bar
1.256 \rail@nextbar{1}
1.257 @@ -1566,7 +1566,7 @@
1.258 later.
1.259
1.260 \begin{railoutput}
1.261 -\rail@begin{4}{\isa{}}
1.262 +\rail@begin{4}{}
1.263 \rail@term{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}}[]
1.264 \rail@bar
1.265 \rail@nont{\isa{caseref}}[]
1.266 @@ -1591,14 +1591,14 @@
1.267 \rail@nont{\isa{attributes}}[]
1.268 \rail@endbar
1.269 \rail@end
1.270 -\rail@begin{2}{\isa{}}
1.271 +\rail@begin{2}{}
1.272 \rail@term{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}}[]
1.273 \rail@plus
1.274 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.275 \rail@nextplus{1}
1.276 \rail@endplus
1.277 \rail@end
1.278 -\rail@begin{2}{\isa{}}
1.279 +\rail@begin{2}{}
1.280 \rail@term{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}conclusion}}}}[]
1.281 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.282 \rail@plus
1.283 @@ -1606,7 +1606,7 @@
1.284 \rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.285 \rail@endplus
1.286 \rail@end
1.287 -\rail@begin{3}{\isa{}}
1.288 +\rail@begin{3}{}
1.289 \rail@term{\hyperlink{attribute.params}{\mbox{\isa{params}}}}[]
1.290 \rail@plus
1.291 \rail@plus
1.292 @@ -1617,7 +1617,7 @@
1.293 \rail@cterm{\isa{\isakeyword{and}}}[]
1.294 \rail@endplus
1.295 \rail@end
1.296 -\rail@begin{2}{\isa{}}
1.297 +\rail@begin{2}{}
1.298 \rail@term{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}}[]
1.299 \rail@bar
1.300 \rail@nextbar{1}
1.301 @@ -1700,7 +1700,7 @@
1.302 ``strengthened'' inductive statements within the object-logic.
1.303
1.304 \begin{railoutput}
1.305 -\rail@begin{3}{\isa{}}
1.306 +\rail@begin{3}{}
1.307 \rail@term{\hyperlink{method.cases}{\mbox{\isa{cases}}}}[]
1.308 \rail@bar
1.309 \rail@nextbar{1}
1.310 @@ -1721,7 +1721,7 @@
1.311 \rail@nont{\isa{rule}}[]
1.312 \rail@endbar
1.313 \rail@end
1.314 -\rail@begin{6}{\isa{}}
1.315 +\rail@begin{6}{}
1.316 \rail@term{\hyperlink{method.induct}{\mbox{\isa{induct}}}}[]
1.317 \rail@bar
1.318 \rail@nextbar{1}
1.319 @@ -1751,7 +1751,7 @@
1.320 \rail@nont{\isa{rule}}[]
1.321 \rail@endbar
1.322 \rail@end
1.323 -\rail@begin{2}{\isa{}}
1.324 +\rail@begin{2}{}
1.325 \rail@term{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}}[]
1.326 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
1.327 \rail@nont{\isa{taking}}[]
1.328 @@ -1987,15 +1987,15 @@
1.329 \end{matharray}
1.330
1.331 \begin{railoutput}
1.332 -\rail@begin{1}{\isa{}}
1.333 +\rail@begin{1}{}
1.334 \rail@term{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}}[]
1.335 \rail@nont{\isa{spec}}[]
1.336 \rail@end
1.337 -\rail@begin{1}{\isa{}}
1.338 +\rail@begin{1}{}
1.339 \rail@term{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}}[]
1.340 \rail@nont{\isa{spec}}[]
1.341 \rail@end
1.342 -\rail@begin{1}{\isa{}}
1.343 +\rail@begin{1}{}
1.344 \rail@term{\hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}}[]
1.345 \rail@nont{\isa{spec}}[]
1.346 \rail@end