replaced macros by antiquotations;
authorwenzelm
Fri, 09 May 2008 23:19:20 +0200
changeset 26864 1417e704d724
parent 26863 cc779d3da712
child 26865 a3afbb414b69
replaced macros by antiquotations;
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}