--- a/doc-src/IsarRef/pure.tex Thu Feb 16 18:25:55 2006 +0100
+++ b/doc-src/IsarRef/pure.tex Thu Feb 16 18:25:55 2006 +0100
@@ -106,12 +106,12 @@
\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}
\indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{text-raw}
\begin{matharray}{rcl}
- \isarcmd{chapter} & : & \isartrans{theory}{theory} \\
- \isarcmd{section} & : & \isartrans{theory}{theory} \\
- \isarcmd{subsection} & : & \isartrans{theory}{theory} \\
- \isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\
- \isarcmd{text} & : & \isartrans{theory}{theory} \\
- \isarcmd{text_raw} & : & \isartrans{theory}{theory} \\
+ \isarcmd{chapter} & : & \isarkeep{local{\dsh}theory} \\
+ \isarcmd{section} & : & \isarkeep{local{\dsh}theory} \\
+ \isarcmd{subsection} & : & \isarkeep{local{\dsh}theory} \\
+ \isarcmd{subsubsection} & : & \isarkeep{local{\dsh}theory} \\
+ \isarcmd{text} & : & \isarkeep{local{\dsh}theory} \\
+ \isarcmd{text_raw} & : & \isarkeep{local{\dsh}theory} \\
\end{matharray}
Apart from formal comments (see \S\ref{sec:comments}), markup commands provide
@@ -235,7 +235,7 @@
\end{descr}
-\subsection{Constants and simple definitions}\label{sec:consts}
+\subsection{Primitive constants and definitions}\label{sec:consts}
\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}
\begin{matharray}{rcl}