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.
On 30/04/2019 13:22, Christian Sternagel wrote:
>
> In Isabelle2018 the splash screen of Isabelle/jEdit has the X property
>
> _NET_WM_WINDOW_TYPE(ATOM) = _NET_WM_WINDOW_TYPE_DIALOG
>
> while with 2388e0d2827b it has
>
> _NET_WM_WINDOW_TYPE(ATOM) = _NET_WM_WINDOW_TYPE_NORMAL
>
> This
