Re: [isabelle] Isabelle2013-RC2 available for testing

On 02/06/2013 11:01 AM, Yannick Duchêne (Hibou57) wrote:
Tiny mistake in “logics-HOL.pdf”. On page 8, it says “someI” is part of
HOL. It's not, it's in Main.

To answer in a confusing way: Main is HOL ;)

But seriously. In the PDF, "HOL" refers to the logic HOL (not to the theory file HOL.thy). And everything that is loaded by Main.thy (including the theory Hilbert_Choice.thy, which adds "someI") is part of the logic image HOL, and thus of the logic HOL as used in Isabelle/HOL. (Additionally there are of course extensions like theories from ~~/src/HOL/Library or the AFP, but what Main.thy represents is kind of the minimal version that a user should see.)

hope this helps,


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