On 01/02/2019 16:40, Lars Hupel wrote: >> The standard approach for the latter is to have the other tool directly >> import its source format into the theory context within Isabelle/ML, >> without the intermediate theory source. Doing this carefully, would even >> produce nice PIDE markup for the original sources. PIDE is an IDE for >> arbitrary user-defined languages. >> >> It might be worth doing this for tools like Lem eventually, but I have >> not looked at it closely so far. > > Lem is implemented in OCaml, so this seems like a stretch. I'd say > importing HOL4 into Isabelle is a more plausible solution.
Yes, the motivation behind using Lem is diminished by the promising work of Fabian Immler. In general, though, alien tool output can be imported into the formal context. One merely needs to devise some tricks. A tool implemented in Haskell or OCaml should be particularly easy. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev