Re: [isabelle] Replacing COMP



On Thu, 1 Aug 2013, René Neumann wrote:

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?

No, I merely dropped the old-style Latex @i of Larry when updating the manual last November. This "painting" of informal text is not machine-checked, so it can occasionally break down.


	Makarius


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