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
