On 21/12/10 15:49 , Osman Hasan wrote: > Do we have a power function that deals with real powers in > HOL/HOL_light. The function "pow" works on num powers so basically I am > looking for its counterpart that works on real powers.
We don't have this defined, but we do have f(n) = e^n, so you should be able to define exponentiation for arbitrary bases with this and natural logarithm (ln). (See transcTheory.) Please feel free to develop the theory of this constant (I'm not sure what you should call it), and send me something I can add to the bottom of transcScript.sml. Michael ------------------------------------------------------------------------------ Learn how Oracle Real Application Clusters (RAC) One Node allows customers to consolidate database storage, standardize their database environment, and, should the need arise, upgrade to a full multi-node Oracle RAC database without downtime or disruption http://p.sf.net/sfu/oracle-sfdevnl _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
