--- 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";