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
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA256
Dear colleagues,
At the 4th International Congress on Mathematical Software (which is a
satellite conference to the International Mathematical Congress) we
will organize a special session on
"Software for Mathematical Theory Exploration" (and rela
===
FIRST CALL FOR PARTICIPATION
Fourth International SAT/SMT Summer School
Semmering, Austria, July 10-12, 2014
http://satsmt2014.forsyte.at/
===
REGISTRATION:
The registration deadline for the summer school
On 17 Mar 2014, at 00:52, Konrad Slind wrote:
> RE: type bool. I think BOOL_CASES_AX can be derived from choice.
> There's a topos-flavoured proof (due to Diaconescu?) in Lambek and Scott,
> which I think John ported to HOL-Light.
Yes. I don’t know the right reference: the comment in the HOL Li
