# HG changeset patch
# User nipkow
# Date 990180833 -7200
# Node ID 891fbd3f48813d2beb83404687c999103ad92ce4
# Parent  6f4ed75b2dcaf8a459878925a46ebc33c6c27a7f
*** empty log message ***

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