1.1 --- a/doc-src/IsarImplementation/Thy/document/Logic.tex Tue May 03 20:59:24 2011 +0200
1.2 +++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Tue May 03 21:07:24 2011 +0200
1.3 @@ -217,15 +217,15 @@
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{ML antiquotation.class}{\mbox{\isa{class}}}}[]
1.10 \rail@nont{\isa{nameref}}[]
1.11 \rail@end
1.12 -\rail@begin{1}{\isa{}}
1.13 +\rail@begin{1}{}
1.14 \rail@term{\hyperlink{ML antiquotation.sort}{\mbox{\isa{sort}}}}[]
1.15 \rail@nont{\isa{sort}}[]
1.16 \rail@end
1.17 -\rail@begin{3}{\isa{}}
1.18 +\rail@begin{3}{}
1.19 \rail@bar
1.20 \rail@term{\hyperlink{ML antiquotation.type-name}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}name}}}}[]
1.21 \rail@nextbar{1}
1.22 @@ -235,7 +235,7 @@
1.23 \rail@endbar
1.24 \rail@nont{\isa{nameref}}[]
1.25 \rail@end
1.26 -\rail@begin{1}{\isa{}}
1.27 +\rail@begin{1}{}
1.28 \rail@term{\hyperlink{ML antiquotation.typ}{\mbox{\isa{typ}}}}[]
1.29 \rail@nont{\isa{type}}[]
1.30 \rail@end
1.31 @@ -481,7 +481,7 @@
1.32 \end{matharray}
1.33
1.34 \begin{railoutput}
1.35 -\rail@begin{2}{\isa{}}
1.36 +\rail@begin{2}{}
1.37 \rail@bar
1.38 \rail@term{\hyperlink{ML antiquotation.const-name}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}name}}}}[]
1.39 \rail@nextbar{1}
1.40 @@ -489,7 +489,7 @@
1.41 \rail@endbar
1.42 \rail@nont{\isa{nameref}}[]
1.43 \rail@end
1.44 -\rail@begin{3}{\isa{}}
1.45 +\rail@begin{3}{}
1.46 \rail@term{\hyperlink{ML antiquotation.const}{\mbox{\isa{const}}}}[]
1.47 \rail@bar
1.48 \rail@nextbar{1}
1.49 @@ -502,11 +502,11 @@
1.50 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.51 \rail@endbar
1.52 \rail@end
1.53 -\rail@begin{1}{\isa{}}
1.54 +\rail@begin{1}{}
1.55 \rail@term{\hyperlink{ML antiquotation.term}{\mbox{\isa{term}}}}[]
1.56 \rail@nont{\isa{term}}[]
1.57 \rail@end
1.58 -\rail@begin{1}{\isa{}}
1.59 +\rail@begin{1}{}
1.60 \rail@term{\hyperlink{ML antiquotation.prop}{\mbox{\isa{prop}}}}[]
1.61 \rail@nont{\isa{prop}}[]
1.62 \rail@end
1.63 @@ -813,27 +813,27 @@
1.64 \end{matharray}
1.65
1.66 \begin{railoutput}
1.67 -\rail@begin{1}{\isa{}}
1.68 +\rail@begin{1}{}
1.69 \rail@term{\hyperlink{ML antiquotation.ctyp}{\mbox{\isa{ctyp}}}}[]
1.70 \rail@nont{\isa{typ}}[]
1.71 \rail@end
1.72 -\rail@begin{1}{\isa{}}
1.73 +\rail@begin{1}{}
1.74 \rail@term{\hyperlink{ML antiquotation.cterm}{\mbox{\isa{cterm}}}}[]
1.75 \rail@nont{\isa{term}}[]
1.76 \rail@end
1.77 -\rail@begin{1}{\isa{}}
1.78 +\rail@begin{1}{}
1.79 \rail@term{\hyperlink{ML antiquotation.cprop}{\mbox{\isa{cprop}}}}[]
1.80 \rail@nont{\isa{prop}}[]
1.81 \rail@end
1.82 -\rail@begin{1}{\isa{}}
1.83 +\rail@begin{1}{}
1.84 \rail@term{\hyperlink{ML antiquotation.thm}{\mbox{\isa{thm}}}}[]
1.85 \rail@nont{\isa{thmref}}[]
1.86 \rail@end
1.87 -\rail@begin{1}{\isa{}}
1.88 +\rail@begin{1}{}
1.89 \rail@term{\hyperlink{ML antiquotation.thms}{\mbox{\isa{thms}}}}[]
1.90 \rail@nont{\isa{thmrefs}}[]
1.91 \rail@end
1.92 -\rail@begin{6}{\isa{}}
1.93 +\rail@begin{6}{}
1.94 \rail@term{\hyperlink{ML antiquotation.lemma}{\mbox{\isa{lemma}}}}[]
1.95 \rail@bar
1.96 \rail@nextbar{1}
2.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex Tue May 03 20:59:24 2011 +0200
2.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Tue May 03 21:07:24 2011 +0200
2.3 @@ -849,7 +849,7 @@
2.4 \end{matharray}
2.5
2.6 \begin{railoutput}
2.7 -\rail@begin{3}{\isa{}}
2.8 +\rail@begin{3}{}
2.9 \rail@term{\hyperlink{ML antiquotation.let}{\mbox{\isa{let}}}}[]
2.10 \rail@plus
2.11 \rail@plus
2.12 @@ -863,7 +863,7 @@
2.13 \rail@cterm{\isa{\isakeyword{and}}}[]
2.14 \rail@endplus
2.15 \rail@end
2.16 -\rail@begin{3}{\isa{}}
2.17 +\rail@begin{3}{}
2.18 \rail@term{\hyperlink{ML antiquotation.note}{\mbox{\isa{note}}}}[]
2.19 \rail@plus
2.20 \rail@bar
3.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Tue May 03 20:59:24 2011 +0200
3.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Tue May 03 21:07:24 2011 +0200
3.3 @@ -265,7 +265,7 @@
3.4 \end{matharray}
3.5
3.6 \begin{railoutput}
3.7 -\rail@begin{2}{\isa{}}
3.8 +\rail@begin{2}{}
3.9 \rail@term{\hyperlink{ML antiquotation.theory}{\mbox{\isa{theory}}}}[]
3.10 \rail@bar
3.11 \rail@nextbar{1}
3.12 @@ -1721,7 +1721,7 @@
3.13 \end{matharray}
3.14
3.15 \begin{railoutput}
3.16 -\rail@begin{1}{\isa{}}
3.17 +\rail@begin{1}{}
3.18 \rail@term{\hyperlink{ML antiquotation.binding}{\mbox{\isa{binding}}}}[]
3.19 \rail@nont{\isa{name}}[]
3.20 \rail@end
4.1 --- a/doc-src/IsarImplementation/Thy/document/Syntax.tex Tue May 03 20:59:24 2011 +0200
4.2 +++ b/doc-src/IsarImplementation/Thy/document/Syntax.tex Tue May 03 21:07:24 2011 +0200
4.3 @@ -168,7 +168,7 @@
4.4 \end{matharray}
4.5
4.6 \begin{railoutput}
4.7 -\rail@begin{4}{\isa{}}
4.8 +\rail@begin{4}{}
4.9 \rail@bar
4.10 \rail@term{\hyperlink{ML antiquotation.class-syntax}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[]
4.11 \rail@nextbar{1}
5.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Tue May 03 20:59:24 2011 +0200
5.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Tue May 03 21:07:24 2011 +0200
5.3 @@ -103,7 +103,7 @@
5.4 syntax.
5.5
5.6 \begin{railoutput}
5.7 -\rail@begin{5}{\isa{}}
5.8 +\rail@begin{5}{}
5.9 \rail@bar
5.10 \rail@term{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}}[]
5.11 \rail@nextbar{1}
5.12 @@ -121,7 +121,7 @@
5.13 \rail@endbar
5.14 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
5.15 \rail@end
5.16 -\rail@begin{7}{\isa{}}
5.17 +\rail@begin{7}{}
5.18 \rail@bar
5.19 \rail@term{\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}}[]
5.20 \rail@nextbar{1}
5.21 @@ -230,7 +230,7 @@
5.22 context.
5.23
5.24 \begin{railoutput}
5.25 -\rail@begin{1}{\isa{}}
5.26 +\rail@begin{1}{}
5.27 \rail@term{\isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}}}[]
5.28 \rail@nont{\isa{antiquotation}}[]
5.29 \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
5.30 @@ -642,7 +642,7 @@
5.31 \end{matharray}
5.32
5.33 \begin{railoutput}
5.34 -\rail@begin{1}{\isa{}}
5.35 +\rail@begin{1}{}
5.36 \rail@term{\isa{rail}}[]
5.37 \rail@nont{\isa{string}}[]
5.38 \rail@end
5.39 @@ -658,7 +658,7 @@
5.40 The rail specification language is quoted here as Isabelle \hyperlink{syntax.string}{\mbox{\isa{string}}}; it has its own grammar given below.
5.41
5.42 \begin{railoutput}
5.43 -\rail@begin{3}{\isa{}}
5.44 +\rail@begin{3}{}
5.45 \rail@plus
5.46 \rail@bar
5.47 \rail@nextbar{1}
5.48 @@ -750,7 +750,7 @@
5.49 \item Empty \verb|()|
5.50
5.51 \begin{railoutput}
5.52 -\rail@begin{1}{\isa{}}
5.53 +\rail@begin{1}{}
5.54 \rail@end
5.55 \end{railoutput}
5.56
5.57 @@ -758,7 +758,7 @@
5.58 \item Nonterminal \verb|A|
5.59
5.60 \begin{railoutput}
5.61 -\rail@begin{1}{\isa{}}
5.62 +\rail@begin{1}{}
5.63 \rail@nont{\isa{A}}[]
5.64 \rail@end
5.65 \end{railoutput}
5.66 @@ -768,7 +768,7 @@
5.67 \verb|@{syntax method}|
5.68
5.69 \begin{railoutput}
5.70 -\rail@begin{1}{\isa{}}
5.71 +\rail@begin{1}{}
5.72 \rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
5.73 \rail@end
5.74 \end{railoutput}
5.75 @@ -777,7 +777,7 @@
5.76 \item Terminal \verb|'xyz'|
5.77
5.78 \begin{railoutput}
5.79 -\rail@begin{1}{\isa{}}
5.80 +\rail@begin{1}{}
5.81 \rail@term{\isa{xyz}}[]
5.82 \rail@end
5.83 \end{railoutput}
5.84 @@ -786,7 +786,7 @@
5.85 \item Terminal in keyword style \verb|@'xyz'|
5.86
5.87 \begin{railoutput}
5.88 -\rail@begin{1}{\isa{}}
5.89 +\rail@begin{1}{}
5.90 \rail@term{\isa{\isakeyword{xyz}}}[]
5.91 \rail@end
5.92 \end{railoutput}
5.93 @@ -796,7 +796,7 @@
5.94 \verb|@@{method rule}|
5.95
5.96 \begin{railoutput}
5.97 -\rail@begin{1}{\isa{}}
5.98 +\rail@begin{1}{}
5.99 \rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
5.100 \rail@end
5.101 \end{railoutput}
5.102 @@ -805,7 +805,7 @@
5.103 \item Concatenation \verb|A B C|
5.104
5.105 \begin{railoutput}
5.106 -\rail@begin{1}{\isa{}}
5.107 +\rail@begin{1}{}
5.108 \rail@nont{\isa{A}}[]
5.109 \rail@nont{\isa{B}}[]
5.110 \rail@nont{\isa{C}}[]
5.111 @@ -819,7 +819,7 @@
5.112 second one for escaping.} \verb|A B C \\ D E F|
5.113
5.114 \begin{railoutput}
5.115 -\rail@begin{3}{\isa{}}
5.116 +\rail@begin{3}{}
5.117 \rail@nont{\isa{A}}[]
5.118 \rail@nont{\isa{B}}[]
5.119 \rail@nont{\isa{C}}[]
5.120 @@ -834,7 +834,7 @@
5.121 \item Variants \verb|A |\verb,|,\verb| B |\verb,|,\verb| C|
5.122
5.123 \begin{railoutput}
5.124 -\rail@begin{3}{\isa{}}
5.125 +\rail@begin{3}{}
5.126 \rail@bar
5.127 \rail@nont{\isa{A}}[]
5.128 \rail@nextbar{1}
5.129 @@ -849,7 +849,7 @@
5.130 \item Option \verb|A ?|
5.131
5.132 \begin{railoutput}
5.133 -\rail@begin{2}{\isa{}}
5.134 +\rail@begin{2}{}
5.135 \rail@bar
5.136 \rail@nextbar{1}
5.137 \rail@nont{\isa{A}}[]
5.138 @@ -861,7 +861,7 @@
5.139 \item Repetition \verb|A *|
5.140
5.141 \begin{railoutput}
5.142 -\rail@begin{2}{\isa{}}
5.143 +\rail@begin{2}{}
5.144 \rail@plus
5.145 \rail@nextplus{1}
5.146 \rail@cnont{\isa{A}}[]
5.147 @@ -873,7 +873,7 @@
5.148 \item Repetition with separator \verb|A * sep|
5.149
5.150 \begin{railoutput}
5.151 -\rail@begin{3}{\isa{}}
5.152 +\rail@begin{3}{}
5.153 \rail@bar
5.154 \rail@nextbar{1}
5.155 \rail@plus
5.156 @@ -889,7 +889,7 @@
5.157 \item Strict repetition \verb|A +|
5.158
5.159 \begin{railoutput}
5.160 -\rail@begin{2}{\isa{}}
5.161 +\rail@begin{2}{}
5.162 \rail@plus
5.163 \rail@nont{\isa{A}}[]
5.164 \rail@nextplus{1}
5.165 @@ -901,7 +901,7 @@
5.166 \item Strict repetition with separator \verb|A + sep|
5.167
5.168 \begin{railoutput}
5.169 -\rail@begin{2}{\isa{}}
5.170 +\rail@begin{2}{}
5.171 \rail@plus
5.172 \rail@nont{\isa{A}}[]
5.173 \rail@nextplus{1}
5.174 @@ -926,7 +926,7 @@
5.175 \end{matharray}
5.176
5.177 \begin{railoutput}
5.178 -\rail@begin{2}{\isa{}}
5.179 +\rail@begin{2}{}
5.180 \rail@bar
5.181 \rail@term{\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isaliteral{5F}{\isacharunderscore}}drafts}}}}}[]
5.182 \rail@nextbar{1}
6.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex Tue May 03 20:59:24 2011 +0200
6.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex Tue May 03 21:07:24 2011 +0200
6.3 @@ -72,7 +72,7 @@
6.4 \end{matharray}
6.5
6.6 \begin{railoutput}
6.7 -\rail@begin{6}{\isa{}}
6.8 +\rail@begin{6}{}
6.9 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
6.10 \rail@bar
6.11 \rail@nextbar{1}
6.12 @@ -128,7 +128,7 @@
6.13 \end{matharray}
6.14
6.15 \begin{railoutput}
6.16 -\rail@begin{3}{\isa{}}
6.17 +\rail@begin{3}{}
6.18 \rail@bar
6.19 \rail@term{\hyperlink{method.fold}{\mbox{\isa{fold}}}}[]
6.20 \rail@nextbar{1}
6.21 @@ -138,7 +138,7 @@
6.22 \rail@endbar
6.23 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
6.24 \rail@end
6.25 -\rail@begin{3}{\isa{}}
6.26 +\rail@begin{3}{}
6.27 \rail@bar
6.28 \rail@term{\hyperlink{method.erule}{\mbox{\isa{erule}}}}[]
6.29 \rail@nextbar{1}
6.30 @@ -206,16 +206,16 @@
6.31 \end{matharray}
6.32
6.33 \begin{railoutput}
6.34 -\rail@begin{1}{\isa{}}
6.35 +\rail@begin{1}{}
6.36 \rail@term{\hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}}[]
6.37 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
6.38 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
6.39 \rail@end
6.40 -\rail@begin{1}{\isa{}}
6.41 +\rail@begin{1}{}
6.42 \rail@term{\hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}}[]
6.43 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
6.44 \rail@end
6.45 -\rail@begin{2}{\isa{}}
6.46 +\rail@begin{2}{}
6.47 \rail@bar
6.48 \rail@term{\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}}[]
6.49 \rail@nextbar{1}
6.50 @@ -229,7 +229,7 @@
6.51 \rail@endbar
6.52 \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
6.53 \rail@end
6.54 -\rail@begin{2}{\isa{}}
6.55 +\rail@begin{2}{}
6.56 \rail@bar
6.57 \rail@term{\hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}}[]
6.58 \rail@nextbar{1}
6.59 @@ -237,7 +237,7 @@
6.60 \rail@endbar
6.61 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
6.62 \rail@end
6.63 -\rail@begin{2}{\isa{}}
6.64 +\rail@begin{2}{}
6.65 \rail@term{\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}}[]
6.66 \rail@bar
6.67 \rail@nextbar{1}
6.68 @@ -297,7 +297,7 @@
6.69 \end{matharray}
6.70
6.71 \begin{railoutput}
6.72 -\rail@begin{3}{\isa{}}
6.73 +\rail@begin{3}{}
6.74 \rail@term{\hyperlink{method.subst}{\mbox{\isa{subst}}}}[]
6.75 \rail@bar
6.76 \rail@nextbar{1}
6.77 @@ -316,7 +316,7 @@
6.78 \rail@endbar
6.79 \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
6.80 \rail@end
6.81 -\rail@begin{2}{\isa{}}
6.82 +\rail@begin{2}{}
6.83 \rail@term{\hyperlink{method.split}{\mbox{\isa{split}}}}[]
6.84 \rail@bar
6.85 \rail@nextbar{1}
6.86 @@ -426,7 +426,7 @@
6.87 \end{matharray}
6.88
6.89 \begin{railoutput}
6.90 -\rail@begin{6}{\isa{}}
6.91 +\rail@begin{6}{}
6.92 \rail@bar
6.93 \rail@term{\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
6.94 \rail@nextbar{1}
6.95 @@ -452,7 +452,7 @@
6.96 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
6.97 \rail@endbar
6.98 \rail@end
6.99 -\rail@begin{2}{\isa{}}
6.100 +\rail@begin{2}{}
6.101 \rail@term{\hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
6.102 \rail@bar
6.103 \rail@nextbar{1}
6.104 @@ -463,7 +463,7 @@
6.105 \rail@nextplus{1}
6.106 \rail@endplus
6.107 \rail@end
6.108 -\rail@begin{2}{\isa{}}
6.109 +\rail@begin{2}{}
6.110 \rail@term{\hyperlink{method.rename-tac}{\mbox{\isa{rename{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
6.111 \rail@bar
6.112 \rail@nextbar{1}
6.113 @@ -474,7 +474,7 @@
6.114 \rail@nextplus{1}
6.115 \rail@endplus
6.116 \rail@end
6.117 -\rail@begin{2}{\isa{}}
6.118 +\rail@begin{2}{}
6.119 \rail@term{\hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
6.120 \rail@bar
6.121 \rail@nextbar{1}
6.122 @@ -485,7 +485,7 @@
6.123 \rail@nont{\hyperlink{syntax.int}{\mbox{\isa{int}}}}[]
6.124 \rail@endbar
6.125 \rail@end
6.126 -\rail@begin{2}{\isa{}}
6.127 +\rail@begin{2}{}
6.128 \rail@bar
6.129 \rail@term{\hyperlink{method.tactic}{\mbox{\isa{tactic}}}}[]
6.130 \rail@nextbar{1}
6.131 @@ -570,7 +570,7 @@
6.132 \end{matharray}
6.133
6.134 \begin{railoutput}
6.135 -\rail@begin{2}{\isa{}}
6.136 +\rail@begin{2}{}
6.137 \rail@bar
6.138 \rail@term{\hyperlink{method.simp}{\mbox{\isa{simp}}}}[]
6.139 \rail@nextbar{1}
6.140 @@ -693,7 +693,7 @@
6.141 \end{matharray}
6.142
6.143 \begin{railoutput}
6.144 -\rail@begin{3}{\isa{}}
6.145 +\rail@begin{3}{}
6.146 \rail@bar
6.147 \rail@term{\hyperlink{attribute.simp}{\mbox{\isa{simp}}}}[]
6.148 \rail@nextbar{1}
6.149 @@ -738,7 +738,7 @@
6.150 \end{matharray}
6.151
6.152 \begin{railoutput}
6.153 -\rail@begin{6}{\isa{}}
6.154 +\rail@begin{6}{}
6.155 \rail@term{\hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
6.156 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
6.157 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
6.158 @@ -760,7 +760,7 @@
6.159 \rail@endplus
6.160 \rail@endbar
6.161 \rail@end
6.162 -\rail@begin{3}{\isa{}}
6.163 +\rail@begin{3}{}
6.164 \rail@term{\hyperlink{attribute.simproc}{\mbox{\isa{simproc}}}}[]
6.165 \rail@bar
6.166 \rail@bar
6.167 @@ -818,7 +818,7 @@
6.168 \end{matharray}
6.169
6.170 \begin{railoutput}
6.171 -\rail@begin{2}{\isa{}}
6.172 +\rail@begin{2}{}
6.173 \rail@term{\hyperlink{attribute.simplified}{\mbox{\isa{simplified}}}}[]
6.174 \rail@bar
6.175 \rail@nextbar{1}
6.176 @@ -877,7 +877,7 @@
6.177 \end{matharray}
6.178
6.179 \begin{railoutput}
6.180 -\rail@begin{3}{\isa{}}
6.181 +\rail@begin{3}{}
6.182 \rail@bar
6.183 \rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
6.184 \rail@nextbar{1}
6.185 @@ -936,7 +936,7 @@
6.186 \end{matharray}
6.187
6.188 \begin{railoutput}
6.189 -\rail@begin{2}{\isa{}}
6.190 +\rail@begin{2}{}
6.191 \rail@term{\hyperlink{method.blast}{\mbox{\isa{blast}}}}[]
6.192 \rail@bar
6.193 \rail@nextbar{1}
6.194 @@ -947,7 +947,7 @@
6.195 \rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[]
6.196 \rail@endplus
6.197 \rail@end
6.198 -\rail@begin{5}{\isa{}}
6.199 +\rail@begin{5}{}
6.200 \rail@bar
6.201 \rail@term{\hyperlink{method.fast}{\mbox{\isa{fast}}}}[]
6.202 \rail@nextbar{1}
6.203 @@ -1022,7 +1022,7 @@
6.204 \end{matharray}
6.205
6.206 \begin{railoutput}
6.207 -\rail@begin{2}{\isa{}}
6.208 +\rail@begin{2}{}
6.209 \rail@term{\hyperlink{method.auto}{\mbox{\isa{auto}}}}[]
6.210 \rail@bar
6.211 \rail@nextbar{1}
6.212 @@ -1034,7 +1034,7 @@
6.213 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
6.214 \rail@endplus
6.215 \rail@end
6.216 -\rail@begin{5}{\isa{}}
6.217 +\rail@begin{5}{}
6.218 \rail@bar
6.219 \rail@term{\hyperlink{method.force}{\mbox{\isa{force}}}}[]
6.220 \rail@nextbar{1}
6.221 @@ -1146,7 +1146,7 @@
6.222 \end{matharray}
6.223
6.224 \begin{railoutput}
6.225 -\rail@begin{3}{\isa{}}
6.226 +\rail@begin{3}{}
6.227 \rail@bar
6.228 \rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[]
6.229 \rail@nextbar{1}
6.230 @@ -1165,11 +1165,11 @@
6.231 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
6.232 \rail@endbar
6.233 \rail@end
6.234 -\rail@begin{1}{\isa{}}
6.235 +\rail@begin{1}{}
6.236 \rail@term{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}}[]
6.237 \rail@term{\isa{del}}[]
6.238 \rail@end
6.239 -\rail@begin{3}{\isa{}}
6.240 +\rail@begin{3}{}
6.241 \rail@term{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}}[]
6.242 \rail@bar
6.243 \rail@bar
6.244 @@ -1272,11 +1272,11 @@
6.245 declarations internally.
6.246
6.247 \begin{railoutput}
6.248 -\rail@begin{1}{\isa{}}
6.249 +\rail@begin{1}{}
6.250 \rail@term{\hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}}[]
6.251 \rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
6.252 \rail@end
6.253 -\rail@begin{2}{\isa{}}
6.254 +\rail@begin{2}{}
6.255 \rail@term{\hyperlink{attribute.atomize}{\mbox{\isa{atomize}}}}[]
6.256 \rail@bar
6.257 \rail@nextbar{1}
6.258 @@ -1285,7 +1285,7 @@
6.259 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
6.260 \rail@endbar
6.261 \rail@end
6.262 -\rail@begin{2}{\isa{}}
6.263 +\rail@begin{2}{}
6.264 \rail@term{\hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
6.265 \rail@bar
6.266 \rail@nextbar{1}
7.1 --- a/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex Tue May 03 20:59:24 2011 +0200
7.2 +++ b/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex Tue May 03 21:07:24 2011 +0200
7.3 @@ -55,7 +55,7 @@
7.4 \end{matharray}
7.5
7.6 \begin{railoutput}
7.7 -\rail@begin{2}{\isa{}}
7.8 +\rail@begin{2}{}
7.9 \rail@term{\hyperlink{command.HOLCF.domain}{\mbox{\isa{\isacommand{domain}}}}}[]
7.10 \rail@bar
7.11 \rail@nextbar{1}
8.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue May 03 20:59:24 2011 +0200
8.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue May 03 21:07:24 2011 +0200
8.3 @@ -32,7 +32,7 @@
8.4 \end{matharray}
8.5
8.6 \begin{railoutput}
8.7 -\rail@begin{2}{\isa{}}
8.8 +\rail@begin{2}{}
8.9 \rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[]
8.10 \rail@bar
8.11 \rail@nextbar{1}
8.12 @@ -123,7 +123,7 @@
8.13 \end{matharray}
8.14
8.15 \begin{railoutput}
8.16 -\rail@begin{2}{\isa{}}
8.17 +\rail@begin{2}{}
8.18 \rail@term{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
8.19 \rail@bar
8.20 \rail@nextbar{1}
8.21 @@ -237,7 +237,7 @@
8.22 \end{matharray}
8.23
8.24 \begin{railoutput}
8.25 -\rail@begin{2}{\isa{}}
8.26 +\rail@begin{2}{}
8.27 \rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]
8.28 \rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
8.29 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
8.30 @@ -410,7 +410,7 @@
8.31 \end{matharray}
8.32
8.33 \begin{railoutput}
8.34 -\rail@begin{2}{\isa{}}
8.35 +\rail@begin{2}{}
8.36 \rail@term{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
8.37 \rail@plus
8.38 \rail@nont{\isa{dtspec}}[]
8.39 @@ -418,7 +418,7 @@
8.40 \rail@cterm{\isa{\isakeyword{and}}}[]
8.41 \rail@endplus
8.42 \rail@end
8.43 -\rail@begin{3}{\isa{}}
8.44 +\rail@begin{3}{}
8.45 \rail@term{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
8.46 \rail@bar
8.47 \rail@nextbar{1}
8.48 @@ -499,7 +499,7 @@
8.49 \end{matharray}
8.50
8.51 \begin{railoutput}
8.52 -\rail@begin{2}{\isa{}}
8.53 +\rail@begin{2}{}
8.54 \rail@term{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
8.55 \rail@bar
8.56 \rail@nextbar{1}
8.57 @@ -552,7 +552,7 @@
8.58 \end{matharray}
8.59
8.60 \begin{railoutput}
8.61 -\rail@begin{2}{\isa{}}
8.62 +\rail@begin{2}{}
8.63 \rail@term{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
8.64 \rail@bar
8.65 \rail@nextbar{1}
8.66 @@ -562,7 +562,7 @@
8.67 \rail@term{\isa{\isakeyword{where}}}[]
8.68 \rail@nont{\isa{equations}}[]
8.69 \rail@end
8.70 -\rail@begin{4}{\isa{}}
8.71 +\rail@begin{4}{}
8.72 \rail@bar
8.73 \rail@term{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}}[]
8.74 \rail@nextbar{1}
8.75 @@ -605,7 +605,7 @@
8.76 \rail@endplus
8.77 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
8.78 \rail@end
8.79 -\rail@begin{2}{\isa{}}
8.80 +\rail@begin{2}{}
8.81 \rail@term{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}}[]
8.82 \rail@bar
8.83 \rail@nextbar{1}
8.84 @@ -696,18 +696,18 @@
8.85 \end{matharray}
8.86
8.87 \begin{railoutput}
8.88 -\rail@begin{1}{\isa{}}
8.89 +\rail@begin{1}{}
8.90 \rail@term{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}}[]
8.91 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
8.92 \rail@end
8.93 -\rail@begin{2}{\isa{}}
8.94 +\rail@begin{2}{}
8.95 \rail@term{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}}[]
8.96 \rail@plus
8.97 \rail@nextplus{1}
8.98 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
8.99 \rail@endplus
8.100 \rail@end
8.101 -\rail@begin{2}{\isa{}}
8.102 +\rail@begin{2}{}
8.103 \rail@term{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}}[]
8.104 \rail@nont{\isa{orders}}[]
8.105 \rail@plus
8.106 @@ -781,7 +781,7 @@
8.107 \end{matharray}
8.108
8.109 \begin{railoutput}
8.110 -\rail@begin{5}{\isa{}}
8.111 +\rail@begin{5}{}
8.112 \rail@term{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}}[]
8.113 \rail@bar
8.114 \rail@nextbar{1}
8.115 @@ -866,7 +866,7 @@
8.116 \end{matharray}
8.117
8.118 \begin{railoutput}
8.119 -\rail@begin{5}{\isa{}}
8.120 +\rail@begin{5}{}
8.121 \rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[]
8.122 \rail@bar
8.123 \rail@nextbar{1}
8.124 @@ -886,7 +886,7 @@
8.125 \rail@nont{\isa{hints}}[]
8.126 \rail@endbar
8.127 \rail@end
8.128 -\rail@begin{2}{\isa{}}
8.129 +\rail@begin{2}{}
8.130 \rail@nont{\isa{recdeftc}}[]
8.131 \rail@bar
8.132 \rail@nextbar{1}
8.133 @@ -968,7 +968,7 @@
8.134 \end{matharray}
8.135
8.136 \begin{railoutput}
8.137 -\rail@begin{3}{\isa{}}
8.138 +\rail@begin{3}{}
8.139 \rail@bar
8.140 \rail@term{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}}[]
8.141 \rail@nextbar{1}
8.142 @@ -1023,7 +1023,7 @@
8.143 \end{matharray}
8.144
8.145 \begin{railoutput}
8.146 -\rail@begin{7}{\isa{}}
8.147 +\rail@begin{7}{}
8.148 \rail@bar
8.149 \rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
8.150 \rail@nextbar{1}
8.151 @@ -1066,7 +1066,7 @@
8.152 \rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
8.153 \rail@endplus
8.154 \rail@end
8.155 -\rail@begin{3}{\isa{}}
8.156 +\rail@begin{3}{}
8.157 \rail@term{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}}[]
8.158 \rail@bar
8.159 \rail@nextbar{1}
8.160 @@ -1210,7 +1210,7 @@
8.161 \end{matharray}
8.162
8.163 \begin{railoutput}
8.164 -\rail@begin{2}{\isa{}}
8.165 +\rail@begin{2}{}
8.166 \rail@term{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}}[]
8.167 \rail@plus
8.168 \rail@nextplus{1}
8.169 @@ -1246,7 +1246,7 @@
8.170 \end{matharray}
8.171
8.172 \begin{railoutput}
8.173 -\rail@begin{2}{\isa{}}
8.174 +\rail@begin{2}{}
8.175 \rail@term{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}}[]
8.176 \rail@bar
8.177 \rail@nextbar{1}
8.178 @@ -1281,7 +1281,7 @@
8.179 \end{matharray}
8.180
8.181 \begin{railoutput}
8.182 -\rail@begin{6}{\isa{}}
8.183 +\rail@begin{6}{}
8.184 \rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[]
8.185 \rail@bar
8.186 \rail@nextbar{1}
8.187 @@ -1305,7 +1305,7 @@
8.188 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
8.189 \rail@endbar
8.190 \rail@end
8.191 -\rail@begin{2}{\isa{}}
8.192 +\rail@begin{2}{}
8.193 \rail@term{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}[]
8.194 \rail@bar
8.195 \rail@nextbar{1}
8.196 @@ -1322,7 +1322,7 @@
8.197 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
8.198 \rail@endbar
8.199 \rail@end
8.200 -\rail@begin{2}{\isa{}}
8.201 +\rail@begin{2}{}
8.202 \rail@term{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
8.203 \rail@bar
8.204 \rail@nextbar{1}
8.205 @@ -1407,7 +1407,7 @@
8.206 \end{matharray}
8.207
8.208 \begin{railoutput}
8.209 -\rail@begin{2}{\isa{}}
8.210 +\rail@begin{2}{}
8.211 \rail@term{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}[]
8.212 \rail@bar
8.213 \rail@nextbar{1}
8.214 @@ -1421,7 +1421,7 @@
8.215 \rail@endbar
8.216 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
8.217 \rail@end
8.218 -\rail@begin{3}{\isa{}}
8.219 +\rail@begin{3}{}
8.220 \rail@bar
8.221 \rail@term{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}[]
8.222 \rail@nextbar{1}
8.223 @@ -1440,7 +1440,7 @@
8.224 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
8.225 \rail@endbar
8.226 \rail@end
8.227 -\rail@begin{3}{\isa{}}
8.228 +\rail@begin{3}{}
8.229 \rail@bar
8.230 \rail@term{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
8.231 \rail@nextbar{1}
8.232 @@ -1599,7 +1599,7 @@
8.233 \end{matharray}
8.234
8.235 \begin{railoutput}
8.236 -\rail@begin{2}{\isa{}}
8.237 +\rail@begin{2}{}
8.238 \rail@term{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
8.239 \rail@bar
8.240 \rail@nextbar{1}
8.241 @@ -1611,7 +1611,7 @@
8.242 \rail@nont{\isa{rule}}[]
8.243 \rail@endbar
8.244 \rail@end
8.245 -\rail@begin{3}{\isa{}}
8.246 +\rail@begin{3}{}
8.247 \rail@term{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
8.248 \rail@bar
8.249 \rail@nextbar{1}
8.250 @@ -1630,7 +1630,7 @@
8.251 \rail@nont{\isa{rule}}[]
8.252 \rail@endbar
8.253 \rail@end
8.254 -\rail@begin{3}{\isa{}}
8.255 +\rail@begin{3}{}
8.256 \rail@term{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}[]
8.257 \rail@plus
8.258 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
8.259 @@ -1645,7 +1645,7 @@
8.260 \rail@endplus
8.261 \rail@endbar
8.262 \rail@end
8.263 -\rail@begin{3}{\isa{}}
8.264 +\rail@begin{3}{}
8.265 \rail@term{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[]
8.266 \rail@plus
8.267 \rail@bar
8.268 @@ -1751,7 +1751,7 @@
8.269 \end{matharray}
8.270
8.271 \begin{railoutput}
8.272 -\rail@begin{11}{\isa{}}
8.273 +\rail@begin{11}{}
8.274 \rail@term{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
8.275 \rail@plus
8.276 \rail@nont{\isa{constexpr}}[]
8.277 @@ -1817,7 +1817,7 @@
8.278 \rail@term{\isa{Scala}}[]
8.279 \rail@endbar
8.280 \rail@end
8.281 -\rail@begin{4}{\isa{}}
8.282 +\rail@begin{4}{}
8.283 \rail@term{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}}[]
8.284 \rail@bar
8.285 \rail@nextbar{1}
8.286 @@ -1830,35 +1830,35 @@
8.287 \rail@endbar
8.288 \rail@endbar
8.289 \rail@end
8.290 -\rail@begin{2}{\isa{}}
8.291 +\rail@begin{2}{}
8.292 \rail@term{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}}}[]
8.293 \rail@plus
8.294 \rail@nont{\isa{const}}[]
8.295 \rail@nextplus{1}
8.296 \rail@endplus
8.297 \rail@end
8.298 -\rail@begin{2}{\isa{}}
8.299 +\rail@begin{2}{}
8.300 \rail@term{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
8.301 \rail@plus
8.302 \rail@nont{\isa{const}}[]
8.303 \rail@nextplus{1}
8.304 \rail@endplus
8.305 \rail@end
8.306 -\rail@begin{2}{\isa{}}
8.307 +\rail@begin{2}{}
8.308 \rail@term{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}}}[]
8.309 \rail@bar
8.310 \rail@nextbar{1}
8.311 \rail@term{\isa{del}}[]
8.312 \rail@endbar
8.313 \rail@end
8.314 -\rail@begin{2}{\isa{}}
8.315 +\rail@begin{2}{}
8.316 \rail@term{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}}}[]
8.317 \rail@bar
8.318 \rail@nextbar{1}
8.319 \rail@term{\isa{del}}[]
8.320 \rail@endbar
8.321 \rail@end
8.322 -\rail@begin{3}{\isa{}}
8.323 +\rail@begin{3}{}
8.324 \rail@term{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[]
8.325 \rail@bar
8.326 \rail@nextbar{1}
8.327 @@ -1868,7 +1868,7 @@
8.328 \rail@endplus
8.329 \rail@endbar
8.330 \rail@end
8.331 -\rail@begin{3}{\isa{}}
8.332 +\rail@begin{3}{}
8.333 \rail@term{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
8.334 \rail@bar
8.335 \rail@nextbar{1}
8.336 @@ -1878,7 +1878,7 @@
8.337 \rail@endplus
8.338 \rail@endbar
8.339 \rail@end
8.340 -\rail@begin{7}{\isa{}}
8.341 +\rail@begin{7}{}
8.342 \rail@term{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}}}[]
8.343 \rail@plus
8.344 \rail@nont{\isa{const}}[]
8.345 @@ -1901,7 +1901,7 @@
8.346 \rail@nextplus{6}
8.347 \rail@endplus
8.348 \rail@end
8.349 -\rail@begin{7}{\isa{}}
8.350 +\rail@begin{7}{}
8.351 \rail@term{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
8.352 \rail@plus
8.353 \rail@nont{\isa{typeconstructor}}[]
8.354 @@ -1924,7 +1924,7 @@
8.355 \rail@nextplus{6}
8.356 \rail@endplus
8.357 \rail@end
8.358 -\rail@begin{9}{\isa{}}
8.359 +\rail@begin{9}{}
8.360 \rail@term{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}}}[]
8.361 \rail@plus
8.362 \rail@nont{\isa{class}}[]
8.363 @@ -1948,7 +1948,7 @@
8.364 \rail@nextplus{8}
8.365 \rail@endplus
8.366 \rail@end
8.367 -\rail@begin{7}{\isa{}}
8.368 +\rail@begin{7}{}
8.369 \rail@term{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}}}[]
8.370 \rail@plus
8.371 \rail@nont{\isa{typeconstructor}}[]
8.372 @@ -1973,7 +1973,7 @@
8.373 \rail@nextplus{6}
8.374 \rail@endplus
8.375 \rail@end
8.376 -\rail@begin{2}{\isa{}}
8.377 +\rail@begin{2}{}
8.378 \rail@term{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}}}[]
8.379 \rail@nont{\isa{target}}[]
8.380 \rail@plus
8.381 @@ -1981,13 +1981,13 @@
8.382 \rail@nextplus{1}
8.383 \rail@endplus
8.384 \rail@end
8.385 -\rail@begin{1}{\isa{}}
8.386 +\rail@begin{1}{}
8.387 \rail@term{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}}}[]
8.388 \rail@nont{\isa{const}}[]
8.389 \rail@nont{\isa{const}}[]
8.390 \rail@nont{\isa{target}}[]
8.391 \rail@end
8.392 -\rail@begin{2}{\isa{}}
8.393 +\rail@begin{2}{}
8.394 \rail@term{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}}}[]
8.395 \rail@nont{\isa{target}}[]
8.396 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
8.397 @@ -1997,7 +1997,7 @@
8.398 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
8.399 \rail@endbar
8.400 \rail@end
8.401 -\rail@begin{2}{\isa{}}
8.402 +\rail@begin{2}{}
8.403 \rail@term{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}}}[]
8.404 \rail@nont{\isa{target}}[]
8.405 \rail@plus
8.406 @@ -2006,7 +2006,7 @@
8.407 \rail@nextplus{1}
8.408 \rail@endplus
8.409 \rail@end
8.410 -\rail@begin{11}{\isa{}}
8.411 +\rail@begin{11}{}
8.412 \rail@term{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}}[]
8.413 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
8.414 \rail@cr{2}
8.415 @@ -2189,7 +2189,7 @@
8.416 \end{matharray}
8.417
8.418 \begin{railoutput}
8.419 -\rail@begin{11}{\isa{}}
8.420 +\rail@begin{11}{}
8.421 \rail@bar
8.422 \rail@term{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}}[]
8.423 \rail@nextbar{1}
8.424 @@ -2241,7 +2241,7 @@
8.425 \rail@endplus
8.426 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
8.427 \rail@end
8.428 -\rail@begin{2}{\isa{}}
8.429 +\rail@begin{2}{}
8.430 \rail@term{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
8.431 \rail@plus
8.432 \rail@nont{\isa{codespec}}[]
8.433 @@ -2256,7 +2256,7 @@
8.434 \rail@nont{\isa{attachment}}[]
8.435 \rail@endbar
8.436 \rail@end
8.437 -\rail@begin{2}{\isa{}}
8.438 +\rail@begin{2}{}
8.439 \rail@term{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
8.440 \rail@plus
8.441 \rail@nont{\isa{tycodespec}}[]
8.442 @@ -2289,7 +2289,7 @@
8.443 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
8.444 \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
8.445 \rail@end
8.446 -\rail@begin{2}{\isa{}}
8.447 +\rail@begin{2}{}
8.448 \rail@term{\hyperlink{attribute.code}{\mbox{\isa{code}}}}[]
8.449 \rail@bar
8.450 \rail@nextbar{1}
8.451 @@ -2565,7 +2565,7 @@
8.452 \end{matharray}
8.453
8.454 \begin{railoutput}
8.455 -\rail@begin{6}{\isa{}}
8.456 +\rail@begin{6}{}
8.457 \rail@bar
8.458 \rail@term{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}}[]
8.459 \rail@nextbar{1}
9.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue May 03 20:59:24 2011 +0200
9.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue May 03 21:07:24 2011 +0200
9.3 @@ -45,7 +45,7 @@
9.4 internal logical entities in a human-readable fashion.
9.5
9.6 \begin{railoutput}
9.7 -\rail@begin{2}{\isa{}}
9.8 +\rail@begin{2}{}
9.9 \rail@term{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}[]
9.10 \rail@bar
9.11 \rail@nextbar{1}
9.12 @@ -53,7 +53,7 @@
9.13 \rail@endbar
9.14 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
9.15 \rail@end
9.16 -\rail@begin{2}{\isa{}}
9.17 +\rail@begin{2}{}
9.18 \rail@term{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}[]
9.19 \rail@bar
9.20 \rail@nextbar{1}
9.21 @@ -61,7 +61,7 @@
9.22 \rail@endbar
9.23 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
9.24 \rail@end
9.25 -\rail@begin{2}{\isa{}}
9.26 +\rail@begin{2}{}
9.27 \rail@term{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}[]
9.28 \rail@bar
9.29 \rail@nextbar{1}
9.30 @@ -69,7 +69,7 @@
9.31 \rail@endbar
9.32 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
9.33 \rail@end
9.34 -\rail@begin{2}{\isa{}}
9.35 +\rail@begin{2}{}
9.36 \rail@term{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}[]
9.37 \rail@bar
9.38 \rail@nextbar{1}
9.39 @@ -77,7 +77,7 @@
9.40 \rail@endbar
9.41 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
9.42 \rail@end
9.43 -\rail@begin{2}{\isa{}}
9.44 +\rail@begin{2}{}
9.45 \rail@bar
9.46 \rail@term{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}[]
9.47 \rail@nextbar{1}
9.48 @@ -92,7 +92,7 @@
9.49 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
9.50 \rail@endbar
9.51 \rail@end
9.52 -\rail@begin{2}{\isa{}}
9.53 +\rail@begin{2}{}
9.54 \rail@term{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}[]
9.55 \rail@bar
9.56 \rail@nextbar{1}
9.57 @@ -488,7 +488,7 @@
9.58 \end{matharray}
9.59
9.60 \begin{railoutput}
9.61 -\rail@begin{5}{\isa{}}
9.62 +\rail@begin{5}{}
9.63 \rail@bar
9.64 \rail@term{\hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}notation}}}}}[]
9.65 \rail@nextbar{1}
9.66 @@ -510,7 +510,7 @@
9.67 \rail@cterm{\isa{\isakeyword{and}}}[]
9.68 \rail@endplus
9.69 \rail@end
9.70 -\rail@begin{5}{\isa{}}
9.71 +\rail@begin{5}{}
9.72 \rail@bar
9.73 \rail@term{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}}[]
9.74 \rail@nextbar{1}
9.75 @@ -532,7 +532,7 @@
9.76 \rail@cterm{\isa{\isakeyword{and}}}[]
9.77 \rail@endplus
9.78 \rail@end
9.79 -\rail@begin{2}{\isa{}}
9.80 +\rail@begin{2}{}
9.81 \rail@term{\hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}}}[]
9.82 \rail@bar
9.83 \rail@nextbar{1}
9.84 @@ -899,7 +899,7 @@
9.85 \end{matharray}
9.86
9.87 \begin{railoutput}
9.88 -\rail@begin{2}{\isa{}}
9.89 +\rail@begin{2}{}
9.90 \rail@term{\hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}}[]
9.91 \rail@plus
9.92 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
9.93 @@ -907,7 +907,7 @@
9.94 \rail@cterm{\isa{\isakeyword{and}}}[]
9.95 \rail@endplus
9.96 \rail@end
9.97 -\rail@begin{2}{\isa{}}
9.98 +\rail@begin{2}{}
9.99 \rail@bar
9.100 \rail@term{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}}[]
9.101 \rail@nextbar{1}
9.102 @@ -922,7 +922,7 @@
9.103 \rail@nextplus{1}
9.104 \rail@endplus
9.105 \rail@end
9.106 -\rail@begin{7}{\isa{}}
9.107 +\rail@begin{7}{}
9.108 \rail@bar
9.109 \rail@term{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}}[]
9.110 \rail@nextbar{1}
9.111 @@ -1017,7 +1017,7 @@
9.112 \end{matharray}
9.113
9.114 \begin{railoutput}
9.115 -\rail@begin{5}{\isa{}}
9.116 +\rail@begin{5}{}
9.117 \rail@bar
9.118 \rail@term{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}}}[]
9.119 \rail@nextbar{1}
10.1 --- a/doc-src/IsarRef/Thy/document/Misc.tex Tue May 03 20:59:24 2011 +0200
10.2 +++ b/doc-src/IsarRef/Thy/document/Misc.tex Tue May 03 21:07:24 2011 +0200
10.3 @@ -42,7 +42,7 @@
10.4 \end{matharray}
10.5
10.6 \begin{railoutput}
10.7 -\rail@begin{2}{\isa{}}
10.8 +\rail@begin{2}{}
10.9 \rail@bar
10.10 \rail@term{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theory}}}}}[]
10.11 \rail@nextbar{1}
10.12 @@ -53,7 +53,7 @@
10.13 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
10.14 \rail@endbar
10.15 \rail@end
10.16 -\rail@begin{6}{\isa{}}
10.17 +\rail@begin{6}{}
10.18 \rail@term{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}[]
10.19 \rail@bar
10.20 \rail@nextbar{1}
10.21 @@ -99,7 +99,7 @@
10.22 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
10.23 \rail@endbar
10.24 \rail@end
10.25 -\rail@begin{2}{\isa{}}
10.26 +\rail@begin{2}{}
10.27 \rail@term{\hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}consts}}}}}[]
10.28 \rail@plus
10.29 \rail@nextplus{1}
10.30 @@ -123,11 +123,11 @@
10.31 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
10.32 \rail@endbar
10.33 \rail@end
10.34 -\rail@begin{1}{\isa{}}
10.35 +\rail@begin{1}{}
10.36 \rail@term{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
10.37 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
10.38 \rail@end
10.39 -\rail@begin{3}{\isa{}}
10.40 +\rail@begin{3}{}
10.41 \rail@term{\hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[]
10.42 \rail@bar
10.43 \rail@nextbar{1}
10.44 @@ -259,7 +259,7 @@
10.45 \end{matharray}
10.46
10.47 \begin{railoutput}
10.48 -\rail@begin{2}{\isa{}}
10.49 +\rail@begin{2}{}
10.50 \rail@bar
10.51 \rail@term{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}[]
10.52 \rail@nextbar{1}
11.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex Tue May 03 20:59:24 2011 +0200
11.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Tue May 03 21:07:24 2011 +0200
11.3 @@ -75,11 +75,11 @@
11.4 \end{matharray}
11.5
11.6 \begin{railoutput}
11.7 -\rail@begin{1}{\isa{}}
11.8 +\rail@begin{1}{}
11.9 \rail@term{\hyperlink{command.notepad}{\mbox{\isa{\isacommand{notepad}}}}}[]
11.10 \rail@term{\isa{\isakeyword{begin}}}[]
11.11 \rail@end
11.12 -\rail@begin{1}{\isa{}}
11.13 +\rail@begin{1}{}
11.14 \rail@term{\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}}[]
11.15 \rail@end
11.16 \end{railoutput}
11.17 @@ -220,7 +220,7 @@
11.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}}}.
11.19
11.20 \begin{railoutput}
11.21 -\rail@begin{2}{\isa{}}
11.22 +\rail@begin{2}{}
11.23 \rail@term{\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}}[]
11.24 \rail@plus
11.25 \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
11.26 @@ -228,7 +228,7 @@
11.27 \rail@cterm{\isa{\isakeyword{and}}}[]
11.28 \rail@endplus
11.29 \rail@end
11.30 -\rail@begin{2}{\isa{}}
11.31 +\rail@begin{2}{}
11.32 \rail@bar
11.33 \rail@term{\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}}[]
11.34 \rail@nextbar{1}
11.35 @@ -240,7 +240,7 @@
11.36 \rail@cterm{\isa{\isakeyword{and}}}[]
11.37 \rail@endplus
11.38 \rail@end
11.39 -\rail@begin{2}{\isa{}}
11.40 +\rail@begin{2}{}
11.41 \rail@term{\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}}[]
11.42 \rail@plus
11.43 \rail@nont{\isa{def}}[]
11.44 @@ -331,7 +331,7 @@
11.45 input process just after type checking. Also note that \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} does not support polymorphism.
11.46
11.47 \begin{railoutput}
11.48 -\rail@begin{3}{\isa{}}
11.49 +\rail@begin{3}{}
11.50 \rail@term{\hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}}[]
11.51 \rail@plus
11.52 \rail@plus
11.53 @@ -403,7 +403,7 @@
11.54 issuing a follow-up claim.
11.55
11.56 \begin{railoutput}
11.57 -\rail@begin{3}{\isa{}}
11.58 +\rail@begin{3}{}
11.59 \rail@term{\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}}[]
11.60 \rail@plus
11.61 \rail@bar
11.62 @@ -415,7 +415,7 @@
11.63 \rail@cterm{\isa{\isakeyword{and}}}[]
11.64 \rail@endplus
11.65 \rail@end
11.66 -\rail@begin{4}{\isa{}}
11.67 +\rail@begin{4}{}
11.68 \rail@bar
11.69 \rail@term{\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}}[]
11.70 \rail@nextbar{1}
11.71 @@ -538,7 +538,7 @@
11.72 and assumptions, cf.\ \secref{sec:obtain}).
11.73
11.74 \begin{railoutput}
11.75 -\rail@begin{6}{\isa{}}
11.76 +\rail@begin{6}{}
11.77 \rail@bar
11.78 \rail@term{\hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}}[]
11.79 \rail@nextbar{1}
11.80 @@ -562,7 +562,7 @@
11.81 \rail@nont{\isa{longgoal}}[]
11.82 \rail@endbar
11.83 \rail@end
11.84 -\rail@begin{4}{\isa{}}
11.85 +\rail@begin{4}{}
11.86 \rail@bar
11.87 \rail@term{\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}}[]
11.88 \rail@nextbar{1}
11.89 @@ -574,7 +574,7 @@
11.90 \rail@endbar
11.91 \rail@nont{\isa{goal}}[]
11.92 \rail@end
11.93 -\rail@begin{2}{\isa{}}
11.94 +\rail@begin{2}{}
11.95 \rail@term{\hyperlink{command.print-statement}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}}}}}[]
11.96 \rail@bar
11.97 \rail@nextbar{1}
11.98 @@ -849,21 +849,21 @@
11.99 assumption in the very last step.
11.100
11.101 \begin{railoutput}
11.102 -\rail@begin{2}{\isa{}}
11.103 +\rail@begin{2}{}
11.104 \rail@term{\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}}[]
11.105 \rail@bar
11.106 \rail@nextbar{1}
11.107 \rail@nont{\isa{method}}[]
11.108 \rail@endbar
11.109 \rail@end
11.110 -\rail@begin{2}{\isa{}}
11.111 +\rail@begin{2}{}
11.112 \rail@term{\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}}[]
11.113 \rail@bar
11.114 \rail@nextbar{1}
11.115 \rail@nont{\isa{method}}[]
11.116 \rail@endbar
11.117 \rail@end
11.118 -\rail@begin{2}{\isa{}}
11.119 +\rail@begin{2}{}
11.120 \rail@term{\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}}[]
11.121 \rail@nont{\isa{method}}[]
11.122 \rail@bar
11.123 @@ -871,7 +871,7 @@
11.124 \rail@nont{\isa{method}}[]
11.125 \rail@endbar
11.126 \rail@end
11.127 -\rail@begin{3}{\isa{}}
11.128 +\rail@begin{3}{}
11.129 \rail@bar
11.130 \rail@term{\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}}[]
11.131 \rail@nextbar{1}
11.132 @@ -954,14 +954,14 @@
11.133 \end{matharray}
11.134
11.135 \begin{railoutput}
11.136 -\rail@begin{2}{\isa{}}
11.137 +\rail@begin{2}{}
11.138 \rail@term{\hyperlink{method.fact}{\mbox{\isa{fact}}}}[]
11.139 \rail@bar
11.140 \rail@nextbar{1}
11.141 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
11.142 \rail@endbar
11.143 \rail@end
11.144 -\rail@begin{2}{\isa{}}
11.145 +\rail@begin{2}{}
11.146 \rail@term{\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}}[]
11.147 \rail@bar
11.148 \rail@nextbar{1}
11.149 @@ -993,7 +993,7 @@
11.150 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
11.151 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
11.152 \rail@end
11.153 -\rail@begin{3}{\isa{}}
11.154 +\rail@begin{3}{}
11.155 \rail@bar
11.156 \rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[]
11.157 \rail@nextbar{1}
11.158 @@ -1012,15 +1012,15 @@
11.159 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
11.160 \rail@endbar
11.161 \rail@end
11.162 -\rail@begin{1}{\isa{}}
11.163 +\rail@begin{1}{}
11.164 \rail@term{\hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}}[]
11.165 \rail@term{\isa{del}}[]
11.166 \rail@end
11.167 -\rail@begin{1}{\isa{}}
11.168 +\rail@begin{1}{}
11.169 \rail@term{\hyperlink{attribute.OF}{\mbox{\isa{OF}}}}[]
11.170 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
11.171 \rail@end
11.172 -\rail@begin{2}{\isa{}}
11.173 +\rail@begin{2}{}
11.174 \rail@term{\hyperlink{attribute.of}{\mbox{\isa{of}}}}[]
11.175 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
11.176 \rail@bar
11.177 @@ -1030,7 +1030,7 @@
11.178 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
11.179 \rail@endbar
11.180 \rail@end
11.181 -\rail@begin{6}{\isa{}}
11.182 +\rail@begin{6}{}
11.183 \rail@term{\hyperlink{attribute.where}{\mbox{\isa{where}}}}[]
11.184 \rail@bar
11.185 \rail@nextbar{1}
11.186 @@ -1160,7 +1160,7 @@
11.187 \end{matharray}
11.188
11.189 \begin{railoutput}
11.190 -\rail@begin{2}{\isa{}}
11.191 +\rail@begin{2}{}
11.192 \rail@bar
11.193 \rail@term{\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}}[]
11.194 \rail@nextbar{1}
11.195 @@ -1168,14 +1168,14 @@
11.196 \rail@endbar
11.197 \rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
11.198 \rail@end
11.199 -\rail@begin{2}{\isa{}}
11.200 +\rail@begin{2}{}
11.201 \rail@term{\hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}}}[]
11.202 \rail@bar
11.203 \rail@nextbar{1}
11.204 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
11.205 \rail@endbar
11.206 \rail@end
11.207 -\rail@begin{1}{\isa{}}
11.208 +\rail@begin{1}{}
11.209 \rail@term{\hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}}[]
11.210 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
11.211 \rail@end
11.212 @@ -1234,7 +1234,7 @@
11.213 \end{matharray}
11.214
11.215 \begin{railoutput}
11.216 -\rail@begin{1}{\isa{}}
11.217 +\rail@begin{1}{}
11.218 \rail@term{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
11.219 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
11.220 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
11.221 @@ -1309,7 +1309,7 @@
11.222 occur in the conclusion.
11.223
11.224 \begin{railoutput}
11.225 -\rail@begin{2}{\isa{}}
11.226 +\rail@begin{2}{}
11.227 \rail@term{\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}}[]
11.228 \rail@bar
11.229 \rail@nextbar{1}
11.230 @@ -1327,7 +1327,7 @@
11.231 \rail@cterm{\isa{\isakeyword{and}}}[]
11.232 \rail@endplus
11.233 \rail@end
11.234 -\rail@begin{2}{\isa{}}
11.235 +\rail@begin{2}{}
11.236 \rail@term{\hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}}[]
11.237 \rail@plus
11.238 \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
11.239 @@ -1441,7 +1441,7 @@
11.240 \end{matharray}
11.241
11.242 \begin{railoutput}
11.243 -\rail@begin{2}{\isa{}}
11.244 +\rail@begin{2}{}
11.245 \rail@bar
11.246 \rail@term{\hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}}[]
11.247 \rail@nextbar{1}
11.248 @@ -1454,7 +1454,7 @@
11.249 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
11.250 \rail@endbar
11.251 \rail@end
11.252 -\rail@begin{3}{\isa{}}
11.253 +\rail@begin{3}{}
11.254 \rail@term{\hyperlink{attribute.trans}{\mbox{\isa{trans}}}}[]
11.255 \rail@bar
11.256 \rail@nextbar{1}
11.257 @@ -1566,7 +1566,7 @@
11.258 later.
11.259
11.260 \begin{railoutput}
11.261 -\rail@begin{4}{\isa{}}
11.262 +\rail@begin{4}{}
11.263 \rail@term{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}}[]
11.264 \rail@bar
11.265 \rail@nont{\isa{caseref}}[]
11.266 @@ -1591,14 +1591,14 @@
11.267 \rail@nont{\isa{attributes}}[]
11.268 \rail@endbar
11.269 \rail@end
11.270 -\rail@begin{2}{\isa{}}
11.271 +\rail@begin{2}{}
11.272 \rail@term{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}}[]
11.273 \rail@plus
11.274 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
11.275 \rail@nextplus{1}
11.276 \rail@endplus
11.277 \rail@end
11.278 -\rail@begin{2}{\isa{}}
11.279 +\rail@begin{2}{}
11.280 \rail@term{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}conclusion}}}}[]
11.281 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
11.282 \rail@plus
11.283 @@ -1606,7 +1606,7 @@
11.284 \rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
11.285 \rail@endplus
11.286 \rail@end
11.287 -\rail@begin{3}{\isa{}}
11.288 +\rail@begin{3}{}
11.289 \rail@term{\hyperlink{attribute.params}{\mbox{\isa{params}}}}[]
11.290 \rail@plus
11.291 \rail@plus
11.292 @@ -1617,7 +1617,7 @@
11.293 \rail@cterm{\isa{\isakeyword{and}}}[]
11.294 \rail@endplus
11.295 \rail@end
11.296 -\rail@begin{2}{\isa{}}
11.297 +\rail@begin{2}{}
11.298 \rail@term{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}}[]
11.299 \rail@bar
11.300 \rail@nextbar{1}
11.301 @@ -1700,7 +1700,7 @@
11.302 ``strengthened'' inductive statements within the object-logic.
11.303
11.304 \begin{railoutput}
11.305 -\rail@begin{3}{\isa{}}
11.306 +\rail@begin{3}{}
11.307 \rail@term{\hyperlink{method.cases}{\mbox{\isa{cases}}}}[]
11.308 \rail@bar
11.309 \rail@nextbar{1}
11.310 @@ -1721,7 +1721,7 @@
11.311 \rail@nont{\isa{rule}}[]
11.312 \rail@endbar
11.313 \rail@end
11.314 -\rail@begin{6}{\isa{}}
11.315 +\rail@begin{6}{}
11.316 \rail@term{\hyperlink{method.induct}{\mbox{\isa{induct}}}}[]
11.317 \rail@bar
11.318 \rail@nextbar{1}
11.319 @@ -1751,7 +1751,7 @@
11.320 \rail@nont{\isa{rule}}[]
11.321 \rail@endbar
11.322 \rail@end
11.323 -\rail@begin{2}{\isa{}}
11.324 +\rail@begin{2}{}
11.325 \rail@term{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}}[]
11.326 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
11.327 \rail@nont{\isa{taking}}[]
11.328 @@ -1987,15 +1987,15 @@
11.329 \end{matharray}
11.330
11.331 \begin{railoutput}
11.332 -\rail@begin{1}{\isa{}}
11.333 +\rail@begin{1}{}
11.334 \rail@term{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}}[]
11.335 \rail@nont{\isa{spec}}[]
11.336 \rail@end
11.337 -\rail@begin{1}{\isa{}}
11.338 +\rail@begin{1}{}
11.339 \rail@term{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}}[]
11.340 \rail@nont{\isa{spec}}[]
11.341 \rail@end
11.342 -\rail@begin{1}{\isa{}}
11.343 +\rail@begin{1}{}
11.344 \rail@term{\hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}}[]
11.345 \rail@nont{\isa{spec}}[]
11.346 \rail@end
12.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex Tue May 03 20:59:24 2011 +0200
12.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Tue May 03 21:07:24 2011 +0200
12.3 @@ -69,7 +69,7 @@
12.4 admissible.
12.5
12.6 \begin{railoutput}
12.7 -\rail@begin{2}{\isa{}}
12.8 +\rail@begin{2}{}
12.9 \rail@term{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}}[]
12.10 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
12.11 \rail@term{\isa{\isakeyword{imports}}}[]
12.12 @@ -145,7 +145,7 @@
12.13 \end{matharray}
12.14
12.15 \begin{railoutput}
12.16 -\rail@begin{1}{\isa{}}
12.17 +\rail@begin{1}{}
12.18 \rail@term{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}}[]
12.19 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
12.20 \rail@term{\isa{\isakeyword{begin}}}[]
12.21 @@ -220,7 +220,7 @@
12.22 available, and result names need not be given.
12.23
12.24 \begin{railoutput}
12.25 -\rail@begin{2}{\isa{}}
12.26 +\rail@begin{2}{}
12.27 \rail@term{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}}[]
12.28 \rail@bar
12.29 \rail@nextbar{1}
12.30 @@ -232,7 +232,7 @@
12.31 \rail@nont{\isa{specs}}[]
12.32 \rail@endbar
12.33 \rail@end
12.34 -\rail@begin{2}{\isa{}}
12.35 +\rail@begin{2}{}
12.36 \rail@term{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}}[]
12.37 \rail@bar
12.38 \rail@nextbar{1}
12.39 @@ -249,7 +249,7 @@
12.40 \rail@endbar
12.41 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
12.42 \rail@end
12.43 -\rail@begin{2}{\isa{}}
12.44 +\rail@begin{2}{}
12.45 \rail@term{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}}[]
12.46 \rail@bar
12.47 \rail@nextbar{1}
12.48 @@ -383,7 +383,7 @@
12.49 \end{matharray}
12.50
12.51 \begin{railoutput}
12.52 -\rail@begin{2}{\isa{}}
12.53 +\rail@begin{2}{}
12.54 \rail@bar
12.55 \rail@term{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}}[]
12.56 \rail@nextbar{1}
12.57 @@ -401,7 +401,7 @@
12.58 \rail@endbar
12.59 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
12.60 \rail@end
12.61 -\rail@begin{2}{\isa{}}
12.62 +\rail@begin{2}{}
12.63 \rail@term{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}}[]
12.64 \rail@bar
12.65 \rail@nextbar{1}
12.66 @@ -568,7 +568,7 @@
12.67 \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
12.68 \indexisarelem{defines}\indexisarelem{notes}
12.69 \begin{railoutput}
12.70 -\rail@begin{2}{\isa{}}
12.71 +\rail@begin{2}{}
12.72 \rail@term{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}}[]
12.73 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
12.74 \rail@bar
12.75 @@ -581,7 +581,7 @@
12.76 \rail@term{\isa{\isakeyword{begin}}}[]
12.77 \rail@endbar
12.78 \rail@end
12.79 -\rail@begin{2}{\isa{}}
12.80 +\rail@begin{2}{}
12.81 \rail@term{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}locale}}}}}[]
12.82 \rail@bar
12.83 \rail@nextbar{1}
12.84 @@ -783,7 +783,7 @@
12.85 \end{matharray}
12.86
12.87 \begin{railoutput}
12.88 -\rail@begin{2}{\isa{}}
12.89 +\rail@begin{2}{}
12.90 \rail@term{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}}[]
12.91 \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
12.92 \rail@bar
12.93 @@ -791,7 +791,7 @@
12.94 \rail@nont{\isa{equations}}[]
12.95 \rail@endbar
12.96 \rail@end
12.97 -\rail@begin{2}{\isa{}}
12.98 +\rail@begin{2}{}
12.99 \rail@term{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}}[]
12.100 \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
12.101 \rail@bar
12.102 @@ -799,7 +799,7 @@
12.103 \rail@nont{\isa{equations}}[]
12.104 \rail@endbar
12.105 \rail@end
12.106 -\rail@begin{2}{\isa{}}
12.107 +\rail@begin{2}{}
12.108 \rail@term{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}}[]
12.109 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
12.110 \rail@bar
12.111 @@ -813,7 +813,7 @@
12.112 \rail@nont{\isa{equations}}[]
12.113 \rail@endbar
12.114 \rail@end
12.115 -\rail@begin{2}{\isa{}}
12.116 +\rail@begin{2}{}
12.117 \rail@term{\hyperlink{command.print-dependencies}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}dependencies}}}}}[]
12.118 \rail@bar
12.119 \rail@nextbar{1}
12.120 @@ -821,7 +821,7 @@
12.121 \rail@endbar
12.122 \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
12.123 \rail@end
12.124 -\rail@begin{1}{\isa{}}
12.125 +\rail@begin{1}{}
12.126 \rail@term{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}}[]
12.127 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
12.128 \rail@end
12.129 @@ -965,7 +965,7 @@
12.130 \end{matharray}
12.131
12.132 \begin{railoutput}
12.133 -\rail@begin{8}{\isa{}}
12.134 +\rail@begin{8}{}
12.135 \rail@term{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}}[]
12.136 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
12.137 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
12.138 @@ -990,7 +990,7 @@
12.139 \rail@term{\isa{\isakeyword{begin}}}[]
12.140 \rail@endbar
12.141 \rail@end
12.142 -\rail@begin{2}{\isa{}}
12.143 +\rail@begin{2}{}
12.144 \rail@term{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}}[]
12.145 \rail@plus
12.146 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
12.147 @@ -1001,10 +1001,10 @@
12.148 \rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[]
12.149 \rail@term{\isa{\isakeyword{begin}}}[]
12.150 \rail@end
12.151 -\rail@begin{1}{\isa{}}
12.152 +\rail@begin{1}{}
12.153 \rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]
12.154 \rail@end
12.155 -\rail@begin{2}{\isa{}}
12.156 +\rail@begin{2}{}
12.157 \rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]
12.158 \rail@plus
12.159 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
12.160 @@ -1014,7 +1014,7 @@
12.161 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
12.162 \rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[]
12.163 \rail@end
12.164 -\rail@begin{2}{\isa{}}
12.165 +\rail@begin{2}{}
12.166 \rail@term{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}}[]
12.167 \rail@bar
12.168 \rail@nextbar{1}
12.169 @@ -1022,7 +1022,7 @@
12.170 \rail@endbar
12.171 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
12.172 \rail@end
12.173 -\rail@begin{2}{\isa{}}
12.174 +\rail@begin{2}{}
12.175 \rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]
12.176 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
12.177 \rail@bar
12.178 @@ -1032,10 +1032,10 @@
12.179 \rail@endbar
12.180 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
12.181 \rail@end
12.182 -\rail@begin{1}{\isa{}}
12.183 +\rail@begin{1}{}
12.184 \rail@term{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}classes}}}}}[]
12.185 \rail@end
12.186 -\rail@begin{1}{\isa{}}
12.187 +\rail@begin{1}{}
12.188 \rail@term{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
12.189 \rail@end
12.190 \end{railoutput}
12.191 @@ -1197,7 +1197,7 @@
12.192 \end{matharray}
12.193
12.194 \begin{railoutput}
12.195 -\rail@begin{5}{\isa{}}
12.196 +\rail@begin{5}{}
12.197 \rail@term{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}}[]
12.198 \rail@cr{2}
12.199 \rail@plus
12.200 @@ -1259,11 +1259,11 @@
12.201 \end{matharray}
12.202
12.203 \begin{railoutput}
12.204 -\rail@begin{1}{\isa{}}
12.205 +\rail@begin{1}{}
12.206 \rail@term{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}}[]
12.207 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
12.208 \rail@end
12.209 -\rail@begin{6}{\isa{}}
12.210 +\rail@begin{6}{}
12.211 \rail@bar
12.212 \rail@term{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}}[]
12.213 \rail@nextbar{1}
12.214 @@ -1279,7 +1279,7 @@
12.215 \rail@endbar
12.216 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
12.217 \rail@end
12.218 -\rail@begin{1}{\isa{}}
12.219 +\rail@begin{1}{}
12.220 \rail@term{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
12.221 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
12.222 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
12.223 @@ -1383,14 +1383,14 @@
12.224 \end{matharray}
12.225
12.226 \begin{railoutput}
12.227 -\rail@begin{2}{\isa{}}
12.228 +\rail@begin{2}{}
12.229 \rail@term{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}}[]
12.230 \rail@plus
12.231 \rail@nont{\hyperlink{syntax.classdecl}{\mbox{\isa{classdecl}}}}[]
12.232 \rail@nextplus{1}
12.233 \rail@endplus
12.234 \rail@end
12.235 -\rail@begin{3}{\isa{}}
12.236 +\rail@begin{3}{}
12.237 \rail@term{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}}[]
12.238 \rail@plus
12.239 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
12.240 @@ -1404,7 +1404,7 @@
12.241 \rail@cterm{\isa{\isakeyword{and}}}[]
12.242 \rail@endplus
12.243 \rail@end
12.244 -\rail@begin{1}{\isa{}}
12.245 +\rail@begin{1}{}
12.246 \rail@term{\hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isaliteral{5F}{\isacharunderscore}}sort}}}}}[]
12.247 \rail@nont{\hyperlink{syntax.sort}{\mbox{\isa{sort}}}}[]
12.248 \rail@end
12.249 @@ -1453,7 +1453,7 @@
12.250 \end{matharray}
12.251
12.252 \begin{railoutput}
12.253 -\rail@begin{2}{\isa{}}
12.254 +\rail@begin{2}{}
12.255 \rail@term{\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}}}[]
12.256 \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
12.257 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
12.258 @@ -1463,7 +1463,7 @@
12.259 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
12.260 \rail@endbar
12.261 \rail@end
12.262 -\rail@begin{2}{\isa{}}
12.263 +\rail@begin{2}{}
12.264 \rail@term{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}}[]
12.265 \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
12.266 \rail@bar
12.267 @@ -1471,7 +1471,7 @@
12.268 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
12.269 \rail@endbar
12.270 \rail@end
12.271 -\rail@begin{2}{\isa{}}
12.272 +\rail@begin{2}{}
12.273 \rail@term{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}}[]
12.274 \rail@plus
12.275 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
12.276 @@ -1553,7 +1553,7 @@
12.277 \end{matharray}
12.278
12.279 \begin{railoutput}
12.280 -\rail@begin{3}{\isa{}}
12.281 +\rail@begin{3}{}
12.282 \rail@term{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}}[]
12.283 \rail@plus
12.284 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
12.285 @@ -1566,7 +1566,7 @@
12.286 \rail@nextplus{2}
12.287 \rail@endplus
12.288 \rail@end
12.289 -\rail@begin{6}{\isa{}}
12.290 +\rail@begin{6}{}
12.291 \rail@term{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}}[]
12.292 \rail@bar
12.293 \rail@nextbar{1}
12.294 @@ -1626,7 +1626,7 @@
12.295 \end{matharray}
12.296
12.297 \begin{railoutput}
12.298 -\rail@begin{2}{\isa{}}
12.299 +\rail@begin{2}{}
12.300 \rail@term{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}}[]
12.301 \rail@plus
12.302 \rail@nont{\hyperlink{syntax.axmdecl}{\mbox{\isa{axmdecl}}}}[]
12.303 @@ -1634,7 +1634,7 @@
12.304 \rail@nextplus{1}
12.305 \rail@endplus
12.306 \rail@end
12.307 -\rail@begin{3}{\isa{}}
12.308 +\rail@begin{3}{}
12.309 \rail@bar
12.310 \rail@term{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}}[]
12.311 \rail@nextbar{1}
12.312 @@ -1704,7 +1704,7 @@
12.313 \end{matharray}
12.314
12.315 \begin{railoutput}
12.316 -\rail@begin{1}{\isa{}}
12.317 +\rail@begin{1}{}
12.318 \rail@term{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}}[]
12.319 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
12.320 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
12.321 @@ -1743,7 +1743,7 @@
12.322 \end{matharray}
12.323
12.324 \begin{railoutput}
12.325 -\rail@begin{4}{\isa{}}
12.326 +\rail@begin{4}{}
12.327 \rail@bar
12.328 \rail@nont{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}class}}}}}[]
12.329 \rail@nextbar{1}
13.1 --- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex Tue May 03 20:59:24 2011 +0200
13.2 +++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex Tue May 03 21:07:24 2011 +0200
13.3 @@ -40,7 +40,7 @@
13.4 \end{matharray}
13.5
13.6 \begin{railoutput}
13.7 -\rail@begin{3}{\isa{}}
13.8 +\rail@begin{3}{}
13.9 \rail@term{\hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}}}[]
13.10 \rail@bar
13.11 \rail@nextbar{1}
13.12 @@ -88,7 +88,7 @@
13.13 \end{matharray}
13.14
13.15 \begin{railoutput}
13.16 -\rail@begin{2}{\isa{}}
13.17 +\rail@begin{2}{}
13.18 \rail@bar
13.19 \rail@term{\hyperlink{command.ZF.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
13.20 \rail@nextbar{1}
13.21 @@ -163,7 +163,7 @@
13.22 In the following syntax specification \isa{{\isaliteral{22}{\isachardoublequote}}monos{\isaliteral{22}{\isachardoublequote}}}, \isa{typeintros}, and \isa{typeelims} are the same as above.
13.23
13.24 \begin{railoutput}
13.25 -\rail@begin{2}{\isa{}}
13.26 +\rail@begin{2}{}
13.27 \rail@bar
13.28 \rail@term{\hyperlink{command.ZF.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
13.29 \rail@nextbar{1}
13.30 @@ -243,7 +243,7 @@
13.31 \end{matharray}
13.32
13.33 \begin{railoutput}
13.34 -\rail@begin{3}{\isa{}}
13.35 +\rail@begin{3}{}
13.36 \rail@term{\hyperlink{command.ZF.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
13.37 \rail@plus
13.38 \rail@bar
13.39 @@ -274,7 +274,7 @@
13.40 \end{matharray}
13.41
13.42 \begin{railoutput}
13.43 -\rail@begin{2}{\isa{}}
13.44 +\rail@begin{2}{}
13.45 \rail@bar
13.46 \rail@term{\hyperlink{method.ZF.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
13.47 \rail@nextbar{1}
13.48 @@ -286,14 +286,14 @@
13.49 \rail@endbar
13.50 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
13.51 \rail@end
13.52 -\rail@begin{2}{\isa{}}
13.53 +\rail@begin{2}{}
13.54 \rail@term{\hyperlink{method.ZF.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}[]
13.55 \rail@plus
13.56 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
13.57 \rail@nextplus{1}
13.58 \rail@endplus
13.59 \rail@end
13.60 -\rail@begin{3}{\isa{}}
13.61 +\rail@begin{3}{}
13.62 \rail@term{\hyperlink{command.ZF.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[]
13.63 \rail@plus
13.64 \rail@bar