*** empty log message ***
Mon, 14 Aug 2006 11:16:20 +0200
changeset 20375 e91be828ce4e
parent 20374 01b711328990
child 20376 53b31f7c1d87
*** empty log message ***
--- 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.