*** empty log message ***
authornipkow
Fri May 18 12:13:53 2001 +0200 (2001-05-18)
changeset 11307891fbd3f4881
parent 11306 6f4ed75b2dca
child 11308 b28bbb153603
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Fri May 18 12:09:13 2001 +0200
     1.2 +++ b/NEWS	Fri May 18 12:13:53 2001 +0200
     1.3 @@ -1,6 +1,11 @@
     1.4  Isabelle NEWS -- history user-relevant changes
     1.5  ==============================================
     1.6  
     1.7 +* HOL: introduced f^n = f o ... o f
     1.8 +  WARNING: due to the limits of Isabelle's type classes, ^ on functions and
     1.9 +  relations has too general a domain, namely ('a * 'b)set and 'a => 'b.
    1.10 +  This means that it may be necessary to attach explicit type constraints.
    1.11 +
    1.12  * Classical reasoner: renamed addaltern to addafter, addSaltern to addSafter
    1.13  
    1.14  * HOL: added safe wrapper "split_conv_tac" to claset. EXISTING PROOFS MAY FAIL