[isabelle] export_code ... checking

Dear code export experts,

do I assume correctly that

  export_code f1 ... fN checking

can be used to "check" whether code generation "works" (at least to some extend) for constants f1 ... fN. If so, is it an unofficial feature that shouldn't be used in production code?



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