Re: [isabelle] Replacing COMP



Am 31.07.2013 23:48, schrieb Makarius:
> On Wed, 31 Jul 2013, Makarius wrote:
> 
>>> Btw: Reading the implementation manual on Drule.compose. It should
>>> read "The unique s that unifies ψ and φ_i" (i.e. φ_i and not φ),
>>> shouldn't it?
>>
>> Which implementation manual are you reading excactly?  I don't see
>> this in
>> http://isabelle.in.tum.de/dist/Isabelle2013/doc/implementation.pdf
> 
> The above "Drule.compose" (instead of "compose") is probably from some
> arbitrary repository version after the Isabelle2013, but I had already
> dropped the subscript "i" last November when refurbishing really ancient
> material by Larry, so it is not there in the official release.

Yes. In the release version it is just named "compose" without the
Drule. But the rest of text is the same (page 89 near the bottom).

Still wondering: Was dropping the subscript intentional? Or is my
understanding completely off and it is indeed correct without the i?

> In the next release, the old "ref" manual will no longer exist, and its
> remaining material fully absorbed into the isar-ref and implementation
> manuals -- after 5 years of working on that.

I don't get the context (from the rest of the mail/thread), but
congratulation.

- René

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift



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