
diff -r fdffd7c40864 -r 946ef711dc7d doc-src/IsarRef/pure.tex
--- 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}




