Konrad and Rob have already answered Bill very thoroughly, but I'll add
two additional comments:
1. I guess Bill was dicombobulated by the "..._AX" name, which does
suggest an axiom. This name is for historical reasons and compatibility
with other HOLs. BOOL_CASES_AX was traditionally a true axiom in HOL
from the early days, and probably still is in some other versions.
2. The argument formerly used a direct port of the original Diaconescu
proof as presented in Beeson's "Foundations of Constructive Mathematics".
But in July 2009 I changed it to a somewhat optimized variant shown to
me by Mark Adams. This is noted in the CHANGES file but not in the
comments (I'll fix that).
John.
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
