# HG changeset patch
# User wenzelm
# Date 969980632 -7200
# Node ID 8fb8c17d1cb5a6077b6f175af7e9c7959692527f
# Parent  0d78784176f492c2861b1c59487356145c702866
HOL/MicroJava;

diff -r 0d78784176f4 -r 8fb8c17d1cb5 NEWS
--- a/NEWS	Tue Sep 26 17:02:51 2000 +0200
+++ b/NEWS	Tue Sep 26 17:03:52 2000 +0200
@@ -225,6 +225,13 @@
 
 *** HOL ***
 
+* HOL/MicroJava: formalization of a fragment of Java, together with a
+corresponding virtual machine and a specification of its bytecode
+verifier and a lightweight bytecode verifier, including proofs of
+type-safety; by Gerwin Klein, Tobias Nipkow, David von Oheimb, and
+Cornelia Pusch (see also the homepage of project Bali at
+http://isabelle.in.tum.de/Bali/);
+
 * HOL/Algebra: new theory of rings and univariate polynomials, by
 Clemens Ballarin;