| changeset 3227 | 9190438471ea |
| parent 3205 | 816a1f9fd620 |
| child 3316 | c2e9ab7d2724 |
--- 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 *;