# HG changeset patch
# User wenzelm
# Date 877450543 -7200
# Node ID ec138de716d9ca7df5d958b5a82668d124dd8ab9
# Parent  edd5ff9371f8fce615291945f2e39e15f6eed269
improved handling of draft signatures / theories; draft thms (and
ctyps, cterms) are automatically promoted to real ones;

diff -r edd5ff9371f8 -r ec138de716d9 NEWS
--- a/NEWS	Tue Oct 21 18:09:13 1997 +0200
+++ b/NEWS	Tue Oct 21 18:15:43 1997 +0200
@@ -28,6 +28,9 @@
 restricted to 'trivial' ones, thus one may have to use
 transfer:theory->thm->thm in (rare) cases;
 
+* improved handling of draft signatures / theories; draft thms (and
+ctyps, cterms) are automatically promoted to real ones;
+
 * slightly changed interfaces for oracles: admit many per theory, named
 (e.g. oracle foo = mlfun), additional name argument for invoke_oracle;