[isabelle-dev] Eisbach and HOL-Analysis

[Makarius]

On 30/04/2019 18:15, Lawrence Paulson wrote:
> This might be very interesting! I assume it’s for proving theorems about distances and norms for type classes such as metric_space and real_normed_vector?
> 
> I don’t know a lot about Eisbach, but it seems to be a fundamental facility so surely there is a case for including it in HOL itself.

Some day Eisbach should be offered as a tool of Pure, but it is still
not ready for that: it requires an ad-hoc change to the "of" attribute,
which still needs to be reconciled with regular "of" in Pure.

This is also the reason why we should not include Eisbach in
HOL-Analysis for Isabelle2019: that session is the basis for many other
things, and it is unclear what can happen out there. We have only a few
days left on that release train, and there are more important things to
spend that time.


	Makarius