HOL: added "The";
authorwenzelm
Fri Jul 20 22:02:45 2001 +0200 (2001-07-20)
changeset 114372338bce575ae
parent 11436 3f74b80d979f
child 11438 3d9222b80989
HOL: added "The";
NEWS
     1.1 --- a/NEWS	Fri Jul 20 22:00:06 2001 +0200
     1.2 +++ b/NEWS	Fri Jul 20 22:02:45 2001 +0200
     1.3 @@ -1,17 +1,22 @@
     1.4 +
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 -* print modes "type_brackets" and "no_type_brackets" control output of nested
     1.9 -=> (types); the default behaviour is "brackets";
    1.10 -
    1.11 -* Classical reasoner: renamed addaltern to addafter, addSaltern to addSafter
    1.12 +* HOL: added "The" definite description operator;
    1.13 +
    1.14 +* print modes "type_brackets" and "no_type_brackets" control output of
    1.15 +nested => (types); the default behaviour is "brackets";
    1.16 +
    1.17 +* Classical reasoner: renamed addaltern to addafter, addSaltern to
    1.18 +addSafter;
    1.19  
    1.20  * HOL: introduced f^n = f o ... o f
    1.21    WARNING: due to the limits of Isabelle's type classes, ^ on functions and
    1.22    relations has too general a domain, namely ('a * 'b)set and 'a => 'b.
    1.23    This means that it may be necessary to attach explicit type constraints.
    1.24  
    1.25 -* HOL: added safe wrapper "split_conv_tac" to claset. EXISTING PROOFS MAY FAIL
    1.26 +* HOL: added safe wrapper "split_conv_tac" to claset.  EXISTING PROOFS
    1.27 +MAY FAIL;
    1.28  
    1.29  * HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this
    1.30    (rare) case use   delSWrapper "split_all_tac" addSbefore