[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 MHonArc.