Thanks for the reference to Piotr R's article, Josef, and I'll read it. Yes. But will they?
I will! I've worked very hard to make my miz3 Hilbert axiomatic geometry code readable, and taking huge leaps nobody could follow would be counterproductive. But I'm against shackling the proof assistant, as we agree Mizar does but miz3 does not: Yes, Mizar is certainly shackled in the way Michael described. I can't figure out your position. I agree there might be some value in shackling for retrieval from huge libraries. Why don't we concentrate on education. I contend that shackling the students' proof assistant is bad design. Michael did not say this, but I say it after listening to Michael, and I'm glad that miz3 is not shackling the students (me, right now). -- Best, Bill ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
