# HG changeset patch
# User wenzelm
# Date 1210367960 -7200
# Node ID 1417e704d724b17e1d82c8bce738debe0654b20f
# Parent  cc779d3da71285eefc8811c5334234055bd983a9
replaced macros by antiquotations;

diff -r cc779d3da712 -r 1417e704d724 doc-src/IsarImplementation/Thy/prelim.thy
--- a/doc-src/IsarImplementation/Thy/prelim.thy	Fri May 09 23:18:52 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/prelim.thy	Fri May 09 23:19:20 2008 +0200
@@ -122,14 +122,14 @@
   @{text "Nat"} &    &              &            & @{text "List"} \\
         & $\searrow$ &              & $\swarrow$ \\
         &            & @{text "Length"} \\
-        &            & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
-        &            & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
+        &            & \multicolumn{3}{l}{~~@{keyword "imports"}} \\
+        &            & \multicolumn{3}{l}{~~@{keyword "begin"}} \\
         &            & $\vdots$~~ \\
         &            & @{text "\<bullet>"}~~ \\
         &            & $\vdots$~~ \\
         &            & @{text "\<bullet>"}~~ \\
         &            & $\vdots$~~ \\
-        &            & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
+        &            & \multicolumn{3}{l}{~~@{command "end"}} \\
   \end{tabular}
   \caption{A theory definition depending on ancestors}\label{fig:ex-theory}
   \end{center}