# HG changeset patch
# User webertj
# Date 1093794131 -7200
# Node ID 73386e0319a2e4bb3c37f94b4e25c35bdf37b594
# Parent  670ab849781826503b341fd74140133140354c80
Provers/blast.ML: depth_limit

diff -r 670ab8497818 -r 73386e0319a2 NEWS
--- a/NEWS	Sun Aug 29 17:36:39 2004 +0200
+++ b/NEWS	Sun Aug 29 17:42:11 2004 +0200
@@ -25,6 +25,9 @@
 * Provers/trancl.ML:  new transitivity reasoner for transitive and
   reflexive-transitive closure of relations.
 
+* Provers/blast.ML:  new reference depth_limit to make blast's depth
+  limit (previously hard-coded with a value of 20) user-definable.
+
 * Pure: considerably improved version of 'constdefs' command.  Now
   performs automatic type-inference of declared constants; additional
   support for local structure declarations (cf. locales and HOL