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