# HG changeset patch
# User wenzelm
# Date 864117885 -7200
# Node ID 9190438471ea60c8dbe96c764f4accb3ba290846
# Parent  04618aca579de10ab76805516fd6220fa5f48864
*** empty log message ***

diff -r 04618aca579d -r 9190438471ea NEWS
--- 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 *;