# HG changeset patch
# User wenzelm
# Date 958669808 -7200
# Node ID c0c583ce0b0b2ad68996bafbe3861832e1fffc45
# Parent  111476895bf2401ed1fc4cfa0eef281a697698c6
* HOL/ML: even fewer consts are declared as global (see theories Ord,
Lfp, Gfp, WF); this only affects ML packages that refer to const names
internally;
* 'pr' command: no longer prints theory contexts, but only proof
states;

diff -r 111476895bf2 -r c0c583ce0b0b NEWS
--- a/NEWS	Thu May 18 19:04:04 2000 +0200
+++ b/NEWS	Thu May 18 19:10:08 2000 +0200
@@ -31,6 +31,10 @@
 
 * HOL/Real: "rabs" replaced by overloaded "abs" function;
 
+* HOL/ML: even fewer consts are declared as global (see theories Ord,
+Lfp, Gfp, WF); this only affects ML packages that refer to const names
+internally;
+
 * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
 
 * LaTeX: several improvements of isabelle.sty;
@@ -87,7 +91,8 @@
 
 * Provers: intro/elim/dest attributes: changed ! / !! flags to ? / ??;
 
-* 'pr' command: optional goals_limit argument;
+* 'pr' command: optional goals_limit argument; no longer prints theory
+contexts, but only proof states;
 
 * diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit
 additional print modes to be specified; e.g. "pr(latex)" will print
@@ -154,6 +159,9 @@
 * theory Sexp now in HOL/Induct examples (used to be part of main HOL,
 but was unused);
 
+* fewer consts declared as global (e.g. have to refer to "Lfp.lfp"
+instead of "lfp" internally; affects ML packages only);
+
 
 *** General ***