# HG changeset patch
# User wenzelm
# Date 1030438761 -7200
# Node ID 934fffeb6f386b55504000fb4ca4946296ffe887
# Parent  1aaa14d7a4b9581d08167b0a2fc316653c031f6f
* Isar: preview of problems to finish 'show' now produce an error

diff -r 1aaa14d7a4b9 -r 934fffeb6f38 NEWS
--- a/NEWS	Sat Aug 24 18:53:43 2002 +0200
+++ b/NEWS	Tue Aug 27 10:59:21 2002 +0200
@@ -1,3 +1,4 @@
+
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
@@ -28,14 +29,17 @@
 "foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from
 the goal statement); "foo" still refers to all facts collectively;
 
+* Isar: preview of problems to finish 'show' now produce an error
+rather than just a warning (in interactive mode);
+
 
 *** HOL ***
 
 * 'typedef' command has new option "open" to suppress the set
 definition;
 
-* Functions Min and Max on finite sets have been introduced.
-  (theory Finite_Set)
+* functions Min and Max on finite sets have been introduced (theory
+Finite_Set);
 
 * attribute [symmetric] now works for relations as well; it turns
 (x,y) : R^-1 into (y,x) : R, and vice versa;