
<html><head></head><body>There is already one for norms (the method norm), and this one would be for dist.<br><br>Fabian<br><br><div class="gmail_quote">On April 30, 2019 6:15:09 PM GMT+02:00, Lawrence Paulson <lp15@cam.ac.uk> wrote:<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">

<pre class="k9mail">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?<br><br>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.<br><br>Larry<br><br><blockquote class="gmail_quote" style="margin: 0pt 0pt 1ex 0.8ex; border-left: 1px solid #729fcf; padding-left: 1ex;">On 30 Apr 2019, at 16:33, Fabian Immler <immler@in.tum.de> wrote:<br><br>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.<br></blockquote><br></pre></blockquote></div></body></html>