Re: [isabelle] code-relect features



Dear Yongjian,

For this example to work you need to include the theory

  "~~/src/HOL/Library/Efficient_Nat"

in the imports-section of your theory.

Hope this helps,
Christian


On Tuesday, June 19, 2012 at 18:20:13 (+0800), li yongjian wrote:
 > Dear urban:
 > 
 >    I'm trying the code_reflect features.
 > 
 >   But there is still type erros.
 > 
 >    COuld you please take time to view it.
 > 
 > See attachment
 > xuntyped binary data, machineLearnin [Press RETURN to save to a file]

-- 





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