[isabelle-dev] Eisbach and HOL-Analysis

[Fabian Immler]

There is already one for norms (the method norm), and this one would be for dist.

Fabian

On April 30, 2019 6:15:09 PM GMT+02:00, Lawrence Paulson <lp15 at cam.ac.uk> 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.
>
>Larry
>
>> On 30 Apr 2019, at 16:33, Fabian Immler <immler at in.tum.de> wrote:
>> 
>> Maximilian (in cc) ported HOL-Light's decision procedure for metric
>spaces [1], and currently has two prototype implementations, one in
>Isabelle/ML, and the other one as an Eisbach method.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190430/4c22c987/attachment.html>