[isabelle] newbie questions r.e. Isar to Haskell/ML generation


I am new to Isabelle/HOL and Isar in general although I know the principles
and am familiar with languages like Z. And with Haskell and ML.

I am trying to work out how to use the jEdit IDE, but would prefer to work
from command line as well.

How do I generate Haskell and ML and friends from a proof like CoreC++ for
example ?

Many thanks in advance,


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.