diff -r 45f837f8889d -r 879e53d92f51 NEWS --- a/NEWS Tue Jun 05 09:41:11 2001 +0200 +++ b/NEWS Tue Jun 05 09:51:04 2001 +0200 @@ -1,13 +1,16 @@ Isabelle NEWS -- history user-relevant changes ============================================== +* print modes "type_brackets" and "no_type_brackets" control output of nested +=> (types); the default behaviour is "brackets"; + +* Classical reasoner: renamed addaltern to addafter, addSaltern to addSafter + * HOL: introduced f^n = f o ... o f WARNING: due to the limits of Isabelle's type classes, ^ on functions and relations has too general a domain, namely ('a * 'b)set and 'a => 'b. This means that it may be necessary to attach explicit type constraints. -* Classical reasoner: renamed addaltern to addafter, addSaltern to addSafter - * HOL: added safe wrapper "split_conv_tac" to claset. EXISTING PROOFS MAY FAIL * HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this