NEWS
changeset 8887 c0c583ce0b0b
parent 8848 b06d183df34d
child 8921 7c04c98132c4
     1.1 --- a/NEWS	Thu May 18 19:04:04 2000 +0200
     1.2 +++ b/NEWS	Thu May 18 19:10:08 2000 +0200
     1.3 @@ -31,6 +31,10 @@
     1.4  
     1.5  * HOL/Real: "rabs" replaced by overloaded "abs" function;
     1.6  
     1.7 +* HOL/ML: even fewer consts are declared as global (see theories Ord,
     1.8 +Lfp, Gfp, WF); this only affects ML packages that refer to const names
     1.9 +internally;
    1.10 +
    1.11  * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
    1.12  
    1.13  * LaTeX: several improvements of isabelle.sty;
    1.14 @@ -87,7 +91,8 @@
    1.15  
    1.16  * Provers: intro/elim/dest attributes: changed ! / !! flags to ? / ??;
    1.17  
    1.18 -* 'pr' command: optional goals_limit argument;
    1.19 +* 'pr' command: optional goals_limit argument; no longer prints theory
    1.20 +contexts, but only proof states;
    1.21  
    1.22  * diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit
    1.23  additional print modes to be specified; e.g. "pr(latex)" will print
    1.24 @@ -154,6 +159,9 @@
    1.25  * theory Sexp now in HOL/Induct examples (used to be part of main HOL,
    1.26  but was unused);
    1.27  
    1.28 +* fewer consts declared as global (e.g. have to refer to "Lfp.lfp"
    1.29 +instead of "lfp" internally; affects ML packages only);
    1.30 +
    1.31  
    1.32  *** General ***
    1.33