Please document somewhere, but yes. Michael
> On 22 Feb 2016, at 09:24, Ramana Kumar <[email protected]> wrote: > > So, yes? > > On 2 February 2016 at 15:51, Ramana Kumar <[email protected]> wrote: >> On 2 February 2016 at 15:04, Michael Norrish <[email protected]> >> wrote: >>> >>> Don't know. >>> >>> Is it clearly adding functionality we don't have any other way? >> >> >> Yes, I think so. The other way to get the functionality is cumbersome: >> abbreviate lots of your goal and try to instantiate the dependent rewrite >> theorem manually. >> >>> >>> >>> Is it big (makes a difference to Moscow ML); does it contaminate the >>> environment at all (declares new constants; adjusts grammars; adjusts other >>> global elements of the system)? >> >> >> It doesn't touch the logical environment, and I don't think it's very big. >> >> Implicational rewriting (issue #160) would be better, but we don't have >> that. >> >>> >>> >>> Michael >>> >>> On 2 Feb 2016, at 12:17, Ramana Kumar <[email protected]> wrote: >>> >>> Tap tap tap... is this thing on? >>> >>> On 22 January 2016 at 17:56, Ramana Kumar <[email protected]> >>> wrote: >>>> >>>> Would there be any harm in adding dep_rewrite to the standard set of >>>> libraries that are loaded by default? (Similarly to how quantHeuristicsLib >>>> was added some time recently.) >>> >>> >>> >>> ------------------------------------------------------------------------------ >>> Site24x7 APM Insight: Get Deep Visibility into Application Performance >>> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month >>> Monitor end-to-end web transactions and take corrective actions now >>> Troubleshoot faster and improve end-user experience. Signup Now! >>> >>> http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140_______________________________________________ >>> Hol-developers mailing list >>> [email protected] >>> https://lists.sourceforge.net/lists/listinfo/hol-developers >>> >>> >>> >>> ________________________________ >>> >>> The information in this e-mail may be confidential and subject to legal >>> professional privilege and/or copyright. National ICT Australia Limited >>> accepts no liability for any damage caused by this email or its attachments. >> >> ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ------------------------------------------------------------------------------ Site24x7 APM Insight: Get Deep Visibility into Application Performance APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month Monitor end-to-end web transactions and take corrective actions now Troubleshoot faster and improve end-user experience. Signup Now! http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140 _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
