src/HOL/NanoJava/document/root.tex

 \begin{abstract}\noindent
   These theories define {\nJava}, a very small fragment of the programming 
   language Java (with essentially just classes) derived from the one given 
   in \cite{NipkowOP00}.
   For {\nJava}, an operational semantics is given as well as a Hoare logic,
-  which is proved both sound and (relatively) complete. The Hoare logic
+  which is proved both sound and (relatively) complete. 
+  The Hoare logic supports side-effecting expressions and
   implements a new approach for handling auxiliary variables.
   A more complex Hoare logic covering a much larger subset of Java is described
   in \cite{DvO-CPE01}.\\
 See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}.
 \end{abstract}