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
Which implementation manual are you reading excactly? I don't see this
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and