diff -r 6f4ed75b2dca -r 891fbd3f4881 NEWS --- a/NEWS Fri May 18 12:09:13 2001 +0200 +++ b/NEWS Fri May 18 12:13:53 2001 +0200 @@ -1,6 +1,11 @@ Isabelle NEWS -- history user-relevant changes ============================================== +* 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