1.1 --- a/NEWS	Wed Sep 26 20:35:22 2001 +0200
     1.2 +++ b/NEWS	Wed Sep 26 22:24:55 2001 +0200
     1.3 @@ -10,23 +10,32 @@
     1.4  * renamed "antecedent" case to "rule_context";
     1.5  
     1.6  
     1.7 +*** Document preparation ***
     1.8 +
     1.9 +* support bold style (for single symbols only), input syntax is like
    1.10 +this: "\<^bold>\<alpha>" or "\<^bold>A";
    1.11 +
    1.12 +* \<bullet> is no output as bold \cdot by default, which looks much
    1.13 +better in printed text;
    1.14 +
    1.15 +
    1.16  *** HOL ***
    1.17  
    1.18  * HOL: added "The" definite description operator;
    1.19  
    1.20 -* HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this
    1.21 -  (rare) case use   delSWrapper "split_all_tac" addSbefore 
    1.22 -                    ("unsafe_split_all_tac", unsafe_split_all_tac)
    1.23 -
    1.24 -* HOL: added safe wrapper "split_conv_tac" to claset.  EXISTING PROOFS
    1.25 +* HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so
    1.26 +in this (rare) case use:
    1.27 +
    1.28 +  delSWrapper "split_all_tac"
    1.29 +  addSbefore ("unsafe_split_all_tac", unsafe_split_all_tac)
    1.30 +
    1.31 +* HOL: added safe wrapper "split_conv_tac" to claset; EXISTING PROOFS
    1.32  MAY FAIL;
    1.33  
    1.34 -* Classical reasoner: renamed addaltern to addafter, addSaltern to addSafter
    1.35 -
    1.36 -* HOL: introduced f^n = f o ... o f
    1.37 -  WARNING: due to the limits of Isabelle's type classes, ^ on functions and
    1.38 -  relations has too general a domain, namely ('a * 'b)set and 'a => 'b.
    1.39 -  This means that it may be necessary to attach explicit type constraints.
    1.40 +* HOL: introduced f^n = f o ... o f; warning: due to the limits of
    1.41 +Isabelle's type classes, ^ on functions and relations has too general
    1.42 +a domain, namely ('a * 'b) set and 'a => 'b; this means that it may be
    1.43 +necessary to attach explicit type constraints;
    1.44  
    1.45  * HOL: syntax translations now work properly with numerals and records
    1.46  expressions;
    1.47 @@ -47,15 +56,18 @@
    1.48  addSafter;
    1.49  
    1.50  * print modes "type_brackets" and "no_type_brackets" control output of
    1.51 -nested => (types); the default behaviour is "brackets";
    1.52 +nested => (types); the default behavior is "brackets";
    1.53  
    1.54  * Proof General keywords specification is now part of the Isabelle
    1.55  distribution (see etc/isar-keywords.el);
    1.56  
    1.57 -* system: support Poly/ML 4.1.1 (large heaps);
    1.58 +* system: support Poly/ML 4.1.1 (now able to manage large heaps);
    1.59  
    1.60  * system: smart selection of Isabelle process versus Isabelle
    1.61 -interface, accomodates case-insensitive file systems (e.g. HFS+);
    1.62 +interface, accommodates case-insensitive file systems (e.g. HFS+); may
    1.63 +run both "isabelle" and "Isabelle" even if file names are badly
    1.64 +damaged (executable inspects the case of the first letter of its own
    1.65 +name); added separate "isabelle-process" and "isabelle-interface";
    1.66  
    1.67  
    1.68