[isabelle-dev] Eisbach and HOL-Analysis

Lawrence Paulson lp15 at cam.ac.uk
Tue Apr 30 18:15:09 CEST 2019

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 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.

More information about the isabelle-dev mailing list