* ProofContext.prems_limit is now -1 by default;
authorwenzelm
Wed, 09 Aug 2006 10:59:58 +0200
changeset 20370 217aada4f795
parent 20369 7e03c3ed1a18
child 20371 a0f8e89d369d
* ProofContext.prems_limit is now -1 by default;
NEWS
--- a/NEWS	Wed Aug 09 00:14:28 2006 +0200
+++ b/NEWS	Wed Aug 09 10:59:58 2006 +0200
@@ -28,6 +28,13 @@
 
 * Command 'find_theorems': support "*" wildcard in "name:" criterion.
 
+* The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1
+by default, which means that "prems" (and also "fixed variables") are
+suppressed from proof state output.  Note that the ProofGeneral
+settings mechanism allows to change and save options persistently, but
+older versions of Isabelle will fail to start up if a negative prems
+limit is imposed.
+
 
 *** Document preparation ***