Re: [isabelle] Isabelle2013-RC2 available for testing

You are absolutely right. This section describes the primitive HOL theory (HOL.thy). When it was written, Isabelle/HOL followed the traditional formalisation in which the existential quantifier was defined with reference to Hilbert's epsilon operator. Later, the formalisation was changed to eliminate this entirely unnecessary dependence on the axiom of choice, with Hilbert's epsilon being introduced much later in the development. It is now possible to formalise mathematics without use of the axiom of choice in Isabelle/HOL, but you would have to do without a great many things, including Sledgehammer.

Larry Paulson

On 6 Feb 2013, at 02:01, Yannick Duchêne (Hibou57) <yannick_duchene at> wrote:

> Tiny mistake in “logics-HOL.pdf”. On page 8, it says “someI” is part of HOL. It's not, it's in Main.
> -- 
> “Syntactic sugar causes cancer of the semi-colons.” [1]
> “Structured Programming supports the law of the excluded muddle.” [1]
> [1]: Epigrams on Programming — Alan J. — P. Yale University

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