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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
