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.


	Makarius


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