I'm going to consider the matter settled: the real miz3, with timeout = -1, was not weakened by John & Freek. They did not desire to restrict the miz3 "by" to small inference leaps. Arguing that the default timeout of 1 is an intentional weakness has a certainly logical correctness, but it's like saying beer companies intentionally weaken their beer, because in its default state, a beer bottle is useless, and requires a special tool (bottle opener) to obtain value from it.
Up to almost 3600 lines of miz3 Hilbert axiomatic geometry http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz just finished Euclid's Proposition I.16 the Exterior Angle thm. -- 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
