# HG changeset patch
# User wenzelm
# Date 1140110755 -3600
# Node ID 946ef711dc7d2ca764ea4bd8a8dca13f5b212a61
# Parent  fdffd7c408649cdacb41008b5cd71ffc37c612ff
tuned;

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}