*** empty log message ***

--- a/NEWS	Tue May 20 10:39:23 1997 +0200
+++ b/NEWS	Tue May 20 10:44:45 1997 +0200
@@ -105,6 +105,8 @@
 * HOL/ex/LFilter theory of a corecursive "filter" functional for
 infinite lists;
 
+* HOL/Modelcheck demonstrates invocation of model checker oracle;
+
 * HOL/ex/Ring.thy declares cring_simp, which solves equational
 problems in commutative rings, using axiomatic type classes for + and *;