# HG changeset patch
# User wenzelm
# Date 1001535895 -7200
# Node ID 93da54c8a687cda49ff88b2d29fa6c6769b71a8b
# Parent  cb15e46d9c568aed6b1158aabdb6f4d7f6f27006
tuned;

diff -r cb15e46d9c56 -r 93da54c8a687 NEWS
--- a/NEWS	Wed Sep 26 20:35:22 2001 +0200
+++ b/NEWS	Wed Sep 26 22:24:55 2001 +0200
@@ -10,23 +10,32 @@
 * renamed "antecedent" case to "rule_context";
 
 
+*** Document preparation ***
+
+* support bold style (for single symbols only), input syntax is like
+this: "\<^bold>\<alpha>" or "\<^bold>A";
+
+* \<bullet> is no output as bold \cdot by default, which looks much
+better in printed text;
+
+
 *** HOL ***
 
 * HOL: added "The" definite description operator;
 
-* HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this
-  (rare) case use   delSWrapper "split_all_tac" addSbefore 
-                    ("unsafe_split_all_tac", unsafe_split_all_tac)
-
-* HOL: added safe wrapper "split_conv_tac" to claset.  EXISTING PROOFS
+* HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so
+in this (rare) case use:
+
+  delSWrapper "split_all_tac"
+  addSbefore ("unsafe_split_all_tac", unsafe_split_all_tac)
+
+* HOL: added safe wrapper "split_conv_tac" to claset; EXISTING PROOFS
 MAY FAIL;
 
-* 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: 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: syntax translations now work properly with numerals and records
 expressions;
@@ -47,15 +56,18 @@
 addSafter;
 
 * print modes "type_brackets" and "no_type_brackets" control output of
-nested => (types); the default behaviour is "brackets";
+nested => (types); the default behavior is "brackets";
 
 * Proof General keywords specification is now part of the Isabelle
 distribution (see etc/isar-keywords.el);
 
-* system: support Poly/ML 4.1.1 (large heaps);
+* system: support Poly/ML 4.1.1 (now able to manage large heaps);
 
 * system: smart selection of Isabelle process versus Isabelle
-interface, accomodates case-insensitive file systems (e.g. HFS+);
+interface, accommodates case-insensitive file systems (e.g. HFS+); may
+run both "isabelle" and "Isabelle" even if file names are badly
+damaged (executable inspects the case of the first letter of its own
+name); added separate "isabelle-process" and "isabelle-interface";