> 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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
