Re: [isabelle] Need a "What's the foundation of Theory.thy" utility



On 7/10/2013 7:59 AM, "Mark" wrote:
I think it's merely that you don't support Isabelle/HOL.
I do intend to do this, but it requires significant investment.

So maybe you can make it happen. People easily being able to cull out the bogus theories, whether logically correct due to bogus axioms, or illogical due to exploitations and bugs, increases the chances that people will take their time to study the good theories, which will always be necessary for anything that's complicated.

The potential features I've naysayed, I'm sure I would find useful.

I don't see that it could be a bad thing, unless you end up like John MacAfee:

http://arstechnica.com/tech-policy/2013/05/john-mcafee-admits-vice-revealed-his-location-when-fleeing-belize-last-year/

Regards,
GB




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.