1.1 --- a/NEWS	Sat Oct 30 20:39:01 1999 +0200
     1.2 +++ b/NEWS	Sat Oct 30 20:41:30 1999 +0200
     1.3 @@ -1,8 +1,9 @@
     1.4 +
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 -New in this Isabelle version
     1.9 -----------------------------
    1.10 +New in Isabelle99 (October 1999)
    1.11 +--------------------------------
    1.12  
    1.13  *** Overview of INCOMPATIBILITIES (see below for more details) ***
    1.14  
    1.15 @@ -55,12 +56,12 @@
    1.16  
    1.17  *** General ***
    1.18  
    1.19 -* new Isabelle/Isar subsystem provides an alternative to traditional
    1.20 +* New Isabelle/Isar subsystem provides an alternative to traditional
    1.21  tactical theorem proving; together with the ProofGeneral/isar user
    1.22  interface it offers an interactive environment for developing human
    1.23  readable proof documents (Isar == Intelligible semi-automated
    1.24  reasoning); for further information see isatool doc isar-ref,
    1.25 -src/HOL/Isar_examples and http://isabelle.in.tum.de/Isar/;
    1.26 +src/HOL/Isar_examples and http://isabelle.in.tum.de/Isar/
    1.27  
    1.28  * improved presentation of theories: better HTML markup (including
    1.29  colors), graph views in several sizes; isatool usedir now provides a
    1.30 @@ -69,8 +70,7 @@
    1.31  theories only); see isatool doc system for more information;
    1.32  
    1.33  * native support for Proof General, both for classic Isabelle and
    1.34 -Isabelle/Isar (the latter is slightly better supported and more
    1.35 -robust);
    1.36 +Isabelle/Isar;
    1.37  
    1.38  * ML function thm_deps visualizes dependencies of theorems and lemmas,
    1.39  using the graph browser tool;
    1.40 @@ -90,7 +90,7 @@
    1.41  more robust handling of platform specific ML images for SML/NJ;
    1.42  
    1.43  * the settings environment is now statically scoped, i.e. it is never
    1.44 -read again in sub-processes invoked from isabelle, isatool, or
    1.45 +created again in sub-processes invoked from isabelle, isatool, or
    1.46  Isabelle;
    1.47  
    1.48  * path element specification '~~' refers to '$ISABELLE_HOME';
    1.49 @@ -125,8 +125,8 @@
    1.50  * new shorthand tactics ftac, eatac, datac, fatac;
    1.51  
    1.52  * qed (and friends) now accept "" as result name; in that case the
    1.53 -result is not stored, but proper checks and presentation of the result
    1.54 -still apply;
    1.55 +theorem is not stored, but proper checks and presentation of the
    1.56 +result still apply;
    1.57  
    1.58  * theorem database now also indexes constants "Trueprop", "all",
    1.59  "==>", "=="; thus thms_containing, findI etc. may retrieve more rules;
    1.60 @@ -246,8 +246,8 @@
    1.61  HOL/List; hardly an INCOMPATIBILITY since '>>' syntax is used all the
    1.62  time;
    1.63  
    1.64 -* HOL: new tactic smp_tac: int -> int -> tactic, which applies spec several
    1.65 -  times and then mp
    1.66 +* HOL: new tactic smp_tac: int -> int -> tactic, which applies spec
    1.67 +several times and then mp;
    1.68  
    1.69  
    1.70  *** LK ***
    1.71 @@ -317,8 +317,8 @@
    1.72  * proper handling of dangling sort hypotheses (at last!);
    1.73  Thm.strip_shyps and Drule.strip_shyps_warning take care of removing
    1.74  extra sort hypotheses that can be witnessed from the type signature;
    1.75 -the force_strip_shyps is gone, any remaining shyps are simply left in
    1.76 -the theorem (with a warning issued by strip_shyps_warning);
    1.77 +the force_strip_shyps flag is gone, any remaining shyps are simply
    1.78 +left in the theorem (with a warning issued by strip_shyps_warning);
    1.79  
    1.80  
    1.81