Email Gateway (Aug 18 2022 at 10:40): Email Gateway (Aug 18 2022 at 10:40):From: Dominik Luecke <luecke@informatik.uni-bremen.de>
Hello,
I am currently trying to solve some non-linear problems with a
combination of Isabelle and HOL-Light. My intention is to do as much of
the rewriting as possible in Isabelle and and then prove the non-linear
stuff in HOL-Light. My problem is that I have to do the translation of a
intermediate Isabelle proof state to a HOL-Light input by hand.
Is the a neat and simple way to output the current subgoals of a proof
to a file and maybe translate it to another syntax?
Regards,
Dominik
Last updated: May 03 2024 at 01:09 UTC