# 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.