Re: [isabelle] Replacing COMP



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.

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.


	Makarius


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