[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
Many thanks in advance,
This archive was generated by a fusion of
Pipermail (Mailman edition) and