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

Dear Aaron,

Sorry for the late response, I have been out of office for 3 weeks.

theory Code_Generation imports Execute begin
export_code big_step WT WT_i_i_i_o
  in SML module_name CoreCpp
  file "path_to_my_file.ML"

I have the development version built on Ubuntu and checking CoreC++ okay,
but cannot seem to get your above example working. I have tried looking at
the code and managed to get an instance/constant code generated but not the
type system or semantics.

There is no constant 'big_step' or WT_i_i_i_o and it says "No code
equations for WT"
This looks like you are using the Isabelle2012 version of CoreC++ from and not the development version of the AFP from The above code works fine for me with the latter.

Hope this helps,

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