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