Hi Fabian, It is good to know that we are going to have another wonderful decision procedure in Isabelle.
Personally, I will vote for the Isabelle/ML approach, since well-written Isabelle/ML code does not seem much harder to understand (to me) than Eisbach implementations. Also, if we consider the Analysis library a basic library (compared to those in the AFP), reduced dependency might be preferred. Best, Wenda > On 30 Apr 2019, at 16:33, Fabian Immler <[email protected]> wrote: > > Hey everyone, > > 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. > > Now we are wondering which one to finalize and include in HOL-Analysis (the > idea is to use it to automate and simplify proofs about metric spaces in the > library, as well). > > The Eisbach method is more readable and therefore easier to understand and > maintain, but it would pull in Eisbach as an additional dependency. > > Any opinions on whether or not adding Eisbach to the dependencies of > HOL-Analysis would be a bad idea? > > I remember that at some point, importing Eisbach changed the implementation > of the "of" attribute or something like that and therefore caused some > problems down the line. > > (This is probably not relevant for Isabelle2019) > > Best regards, > Fabian > > [1] https://arxiv.org/pdf/0904.3482 > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
