# HG changeset patch
# User wenzelm
# Date 995659365 -7200
# Node ID 2338bce575ae121c3fef491237f6543d456037bf
# Parent  3f74b80d979f7d3ffe2d7bc3c4029ea862ce3591
HOL: added "The";

diff -r 3f74b80d979f -r 2338bce575ae NEWS
--- a/NEWS	Fri Jul 20 22:00:06 2001 +0200
+++ b/NEWS	Fri Jul 20 22:02:45 2001 +0200
@@ -1,17 +1,22 @@
+
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
-* print modes "type_brackets" and "no_type_brackets" control output of nested
-=> (types); the default behaviour is "brackets";
-
-* Classical reasoner: renamed addaltern to addafter, addSaltern to addSafter
+* HOL: added "The" definite description operator;
+
+* print modes "type_brackets" and "no_type_brackets" control output of
+nested => (types); the default behaviour is "brackets";
+
+* Classical reasoner: renamed addaltern to addafter, addSaltern to
+addSafter;
 
 * HOL: introduced f^n = f o ... o f
   WARNING: due to the limits of Isabelle's type classes, ^ on functions and
   relations has too general a domain, namely ('a * 'b)set and 'a => 'b.
   This means that it may be necessary to attach explicit type constraints.
 
-* HOL: added safe wrapper "split_conv_tac" to claset. EXISTING PROOFS MAY FAIL
+* HOL: added safe wrapper "split_conv_tac" to claset.  EXISTING PROOFS
+MAY FAIL;
 
 * HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this
   (rare) case use   delSWrapper "split_all_tac" addSbefore