# HG changeset patch
# User oheimb
# Date 997272756 -7200
# Node ID 4d042d3f957d77c4647b1b4c50eea3f4a23a7843
# Parent 06c1998340a8ba9b8fa90330f7d5d84b9b2c9814
changed to full expressions with side effects
diff -r 06c1998340a8 -r 4d042d3f957d src/HOL/NanoJava/document/root.tex
--- a/src/HOL/NanoJava/document/root.tex Wed Aug 08 12:36:48 2001 +0200
+++ b/src/HOL/NanoJava/document/root.tex Wed Aug 08 14:12:36 2001 +0200
@@ -36,7 +36,8 @@
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}.\\