Dear Michael, Thank you for your encouragement.
(Replying to yours of Sunday, November 11, 2012 8:04 PM >> a caution > to the effect that the addition of new ones to the system requires >> central approval. Can anyone point me to relevant information on the >> design of, and requirements for, HOL libraries? >That language sounds a deal more forbidding than I’d like. Can you point me to >it so it can be fixed/removed? In any case, I’d be quite happy to take >delivery >of source code in whatever form you like. I'm embarrassed, I have mislaid where it was I stumbled across that, which was probably less forbidding than I made it sound. I think a distinction was drawn between libraries and less-overseen things called "contributions". >Ramana earlier mentioned EVAL, also known as CBV_CONV. This aims to allow >efficient rewriting for sets of equations that look like functional programs. >I >imagine your HOL definitions look quite functional so it might be interesting >to >compare the behaviour of the hand-crafted code and EVAL when primed with them. Yes indeed, I intend to try that out. (And see the remainder of my reply to Ramana.) I will send you a copy of the "Notes" (which ought to fission into a paper and a user manual - at the moment they are just everything I could think of to write down) when I send them to him, and my HOL files too if you want to see them, though I don't feel they're in shape yet to speak of "delivering" them. Once I have had Kanasaskis-8 installed here, I will appeal to you for help in connecting to your wellorderTheory. Best Regards, Lockwood ------------------------------------------------------------------------------ Monitor your physical, virtual and cloud infrastructure from a single web console. Get in-depth insight into apps, servers, databases, vmware, SAP, cloud infrastructure, etc. Download 30-day Free Trial. Pricing starts from $795 for 25 servers or applications! http://p.sf.net/sfu/zoho_dev2dev_nov _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
