changeset 11376 bf98ad1c22c6
child 11477 4d042d3f957d
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NanoJava/document/root.tex	Sat Jun 16 20:06:42 2001 +0200
@@ -0,0 +1,57 @@
+%subsection instead of section to make the toc readable
+%remove spaces from the isabelle environment (trivlist makes them too large)
+\newcommand{\nJava}{\it NanoJava}
+%remove clutter from the toc
+\author{David von Oheimb \\ Tobias Nipkow}
+  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
+  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{}.
+\parindent 0pt \parskip 0.5ex