On 20/09/18 11:02, Lars Hupel wrote: > > I'm considering putting the entire CakeML compiler somewhere so that it > is accessible in the AFP.
Just a side-remark: Fabian Immler has started with some experiments to use HOL4 with CakeML inside Isabelle. You should keep in contact with him about progress and possibilities. We can of course discuss such things on the isabelle-dev mailing, when it is relevant to ongoing Isabelle development. Or even on the HOL mailing list, when HOL4 things are touched. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev