Re: [isabelle] Eisbach: HOL vs. Pure
On Mon, 29 Jun 2015, Larry Paulson wrote:
I agree that it would be right for Eisbach to be installed generically,
and available to all object-logics. Everything is Isabelle/HOL these
days, but you never know when Isabelle/ZF might get a small revival. The
original idea of Isabelle is that everything is available everywhere as
much as possible.
Indeed, I still subscribe to this principle. Apart from Isabelle/ZF,
someone might even re-activate the ancient Martin-Löf Type Theory
(Isabelle/CTT), which has become popular again due to the HoTT movement.
The reasons why Eisbach ended up as isolated subsession derived from HOL
are pragmatic. Due to this convenient place in the session hierarchy for
its own development, it was possible to make many last-minute changes and
still ship everything on-time for the release.
Next time it should be done more according to the Pure rules of Isabelle,
but it also requires a second big reform on the instantiation are ("where"
and "of" attributes). More than half of Eisbach are actually just the
usual reforms, to make the application then rather obvious.
This archive was generated by a fusion of
Pipermail (Mailman edition) and