[isabelle] Output of Isabelle Goal-State
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?
Dominik Luecke Phone +49-421-218-64265
Dept. of Computer Science Fax +49-421-218-9864265
University of Bremen luecke at tzi.de
P.O.Box 330440, D-28334 Bremen
PGP-Key ID 0x2D82571B
This archive was generated by a fusion of
Pipermail (Mailman edition) and