# HG changeset patch
# User wenzelm
# Date 1304264541 -7200
# Node ID b68e1c27709a47b5f7d7feafa24a04008c3063fa
# Parent  11417d1eff3b994e0c4206c40422dd0fc50a8ffb
simplified keyword markup (without formal checking);

diff -r 11417d1eff3b -r b68e1c27709a doc-src/IsarImplementation/Thy/Logic.thy
--- 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}
diff -r 11417d1eff3b -r b68e1c27709a doc-src/IsarImplementation/Thy/ML.thy
--- 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}
diff -r 11417d1eff3b -r b68e1c27709a doc-src/IsarImplementation/Thy/document/Logic.tex
--- 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}
diff -r 11417d1eff3b -r b68e1c27709a doc-src/IsarImplementation/Thy/document/ML.tex
--- 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}