NEWS
changeset 11361 879e53d92f51
parent 11314 f6eebbbed449
child 11397 0427e3c88062
     1.1 --- a/NEWS	Tue Jun 05 09:41:11 2001 +0200
     1.2 +++ b/NEWS	Tue Jun 05 09:51:04 2001 +0200
     1.3 @@ -1,13 +1,16 @@
     1.4  Isabelle NEWS -- history user-relevant changes
     1.5  ==============================================
     1.6  
     1.7 +* print modes "type_brackets" and "no_type_brackets" control output of nested
     1.8 +=> (types); the default behaviour is "brackets";
     1.9 +
    1.10 +* Classical reasoner: renamed addaltern to addafter, addSaltern to addSafter
    1.11 +
    1.12  * HOL: introduced f^n = f o ... o f
    1.13    WARNING: due to the limits of Isabelle's type classes, ^ on functions and
    1.14    relations has too general a domain, namely ('a * 'b)set and 'a => 'b.
    1.15    This means that it may be necessary to attach explicit type constraints.
    1.16  
    1.17 -* Classical reasoner: renamed addaltern to addafter, addSaltern to addSafter
    1.18 -
    1.19  * HOL: added safe wrapper "split_conv_tac" to claset. EXISTING PROOFS MAY FAIL
    1.20  
    1.21  * HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this