NEWS
changeset 11633 c8945e0dc00b
parent 11611 b0c69f4db64c
child 11657 03c4a5c08a79
     1.1 --- a/NEWS	Fri Sep 28 19:23:35 2001 +0200
     1.2 +++ b/NEWS	Fri Sep 28 19:23:58 2001 +0200
     1.3 @@ -5,11 +5,6 @@
     1.4  New in Isabelle2001 (?? 2001)
     1.5  -----------------------------
     1.6  
     1.7 -*** Isar ***
     1.8 -
     1.9 -* renamed "antecedent" case to "rule_context";
    1.10 -
    1.11 -
    1.12  *** Document preparation ***
    1.13  
    1.14  * support bold style (for single symbols only), input syntax is like
    1.15 @@ -19,9 +14,21 @@
    1.16  better in printed text;
    1.17  
    1.18  
    1.19 +*** Isar ***
    1.20 +
    1.21 +* Isar/Pure: renamed "antecedent" case to "rule_context";
    1.22 +
    1.23 +* Isar/HOL: 'recdef' now fails on unfinished automated proofs, use
    1.24 +"(permissive)" option to recover old behavior;
    1.25 +
    1.26 +* Isar/HOL: 'inductive' now longer features separate (collective)
    1.27 +attributes for 'intros';
    1.28 +
    1.29 +
    1.30  *** HOL ***
    1.31  
    1.32 -* HOL: added "The" definite description operator;
    1.33 +* HOL: added "The" definite description operator; move Hilbert's "Eps"
    1.34 +to peripheral theory "Hilbert_Choice";
    1.35  
    1.36  * HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so
    1.37  in this (rare) case use:
    1.38 @@ -49,7 +56,6 @@
    1.39    type "unit" -> "Product_Type.unit"
    1.40  
    1.41  
    1.42 -
    1.43  *** ZF ***
    1.44  
    1.45  * ZF: the integer library now covers quotients and remainders, with
    1.46 @@ -58,17 +64,19 @@
    1.47  
    1.48  *** General ***
    1.49  
    1.50 +* Meta-level proof terms (by Stefan Berghofer), see also ref manual;
    1.51 +
    1.52  * Classical reasoner: renamed addaltern to addafter, addSaltern to
    1.53  addSafter;
    1.54  
    1.55  * print modes "type_brackets" and "no_type_brackets" control output of
    1.56  nested => (types); the default behavior is "brackets";
    1.57  
    1.58 -* Proof General keywords specification is now part of the Isabelle
    1.59 -distribution (see etc/isar-keywords.el);
    1.60 -
    1.61  * system: support Poly/ML 4.1.1 (now able to manage large heaps);
    1.62  
    1.63 +* system: Proof General keywords specification is now part of the
    1.64 +Isabelle distribution (see etc/isar-keywords.el);
    1.65 +
    1.66  * system: smart selection of Isabelle process versus Isabelle
    1.67  interface, accommodates case-insensitive file systems (e.g. HFS+); may
    1.68  run both "isabelle" and "Isabelle" even if file names are badly