--- a/doc-src/IsarImplementation/Thy/Logic.thy Sun May 01 17:41:49 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Sun May 01 17:42:21 2011 +0200
@@ -745,8 +745,8 @@
;
@@{ML_antiquotation thms} thmrefs
;
- @@{ML_antiquotation lemma} ('(' @@{keyword \"open\"} ')')? ((prop +) + @@{keyword \"and\"}) \\
- @@{keyword \"by\"} method method?
+ @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \\
+ @'by' method method?
"}
\begin{description}
--- a/doc-src/IsarImplementation/Thy/ML.thy Sun May 01 17:41:49 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Sun May 01 17:42:21 2011 +0200
@@ -699,9 +699,9 @@
\end{matharray}
@{rail "
- @@{ML_antiquotation let} ((term + @@{keyword \"and\"}) '=' term + @@{keyword \"and\"})
+ @@{ML_antiquotation let} ((term + @'and') '=' term + @'and')
;
- @@{ML_antiquotation note} (thmdef? thmrefs + @@{keyword \"and\"})
+ @@{ML_antiquotation note} (thmdef? thmrefs + @'and')
"}
\begin{description}
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Sun May 01 17:41:49 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Sun May 01 17:42:21 2011 +0200
@@ -838,7 +838,7 @@
\rail@bar
\rail@nextbar{1}
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
-\rail@term{\hyperlink{keyword.open}{\mbox{\isa{\isakeyword{open}}}}}[]
+\rail@term{\isa{\isakeyword{open}}}[]
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@endbar
\rail@plus
@@ -847,10 +847,10 @@
\rail@nextplus{1}
\rail@endplus
\rail@nextplus{2}
-\rail@cterm{\hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}}}[]
+\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@cr{4}
-\rail@term{\hyperlink{keyword.by}{\mbox{\isa{\isakeyword{by}}}}}[]
+\rail@term{\isa{\isakeyword{by}}}[]
\rail@nont{\isa{method}}[]
\rail@bar
\rail@nextbar{5}
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Sun May 01 17:41:49 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Sun May 01 17:42:21 2011 +0200
@@ -855,12 +855,12 @@
\rail@plus
\rail@nont{\isa{term}}[]
\rail@nextplus{1}
-\rail@cterm{\hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}}}[]
+\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
\rail@nont{\isa{term}}[]
\rail@nextplus{2}
-\rail@cterm{\hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}}}[]
+\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
\rail@begin{3}{\isa{}}
@@ -872,7 +872,7 @@
\rail@endbar
\rail@nont{\isa{thmrefs}}[]
\rail@nextplus{2}
-\rail@cterm{\hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}}}[]
+\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
\end{railoutput}