# HG changeset patch
# User chaieb
# Date 1155546980 -7200
# Node ID e91be828ce4ed14891b75296126dcb17aaef7a54
# Parent  01b7113289909e551cd731f9077d3143b17e2088
*** empty log message ***

diff -r 01b711328990 -r e91be828ce4e NEWS
--- a/NEWS	Mon Aug 14 11:13:50 2006 +0200
+++ b/NEWS	Mon Aug 14 11:16:20 2006 +0200
@@ -536,6 +536,7 @@
  reflection corr_thm eqs (t). The parameters eqs and (t) are as explained above. corr_thm is a theorem for 
 I vs (f t) = I vs t, where f is supposed to be a computable function (in the sense of code generattion). The method uses reify to compute s and xs as above then applies corr_thm and uses normalization by evaluation to "prove" f s = r and finally gets the theorem t = r, which is again applied to the subgoal. An Example is available in HOL/ex/ReflectionEx.thy.
 
+* Reflection: Automatic refification now handels binding, an example is available in HOL/ex/ReflectionEx.thy
 *** HOL-Algebra ***
 
 * Method algebra is now set up via an attribute.  For examples see CRing.thy.