* Isar: preview of problems to finish 'show' now produce an error
authorwenzelm
Tue Aug 27 10:59:21 2002 +0200 (2002-08-27)
changeset 13522934fffeb6f38
parent 13521 1aaa14d7a4b9
child 13523 079af5c90d1c
* Isar: preview of problems to finish 'show' now produce an error
NEWS
     1.1 --- a/NEWS	Sat Aug 24 18:53:43 2002 +0200
     1.2 +++ b/NEWS	Tue Aug 27 10:59:21 2002 +0200
     1.3 @@ -1,3 +1,4 @@
     1.4 +
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 @@ -28,14 +29,17 @@
     1.9  "foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from
    1.10  the goal statement); "foo" still refers to all facts collectively;
    1.11  
    1.12 +* Isar: preview of problems to finish 'show' now produce an error
    1.13 +rather than just a warning (in interactive mode);
    1.14 +
    1.15  
    1.16  *** HOL ***
    1.17  
    1.18  * 'typedef' command has new option "open" to suppress the set
    1.19  definition;
    1.20  
    1.21 -* Functions Min and Max on finite sets have been introduced.
    1.22 -  (theory Finite_Set)
    1.23 +* functions Min and Max on finite sets have been introduced (theory
    1.24 +Finite_Set);
    1.25  
    1.26  * attribute [symmetric] now works for relations as well; it turns
    1.27  (x,y) : R^-1 into (y,x) : R, and vice versa;