Re: [isabelle] What is sumC?



> Where is code_simp described? It's not in "Programming and Proving in
> Isabelle/HOL"; it's not in "The Isabelle/Isar Reference Manual"; it's
> not in "The Isabelle/Isar Implementation"; it's not in "Isabelle/HOL --
> A Proof Assistant for Higher-Order Logic." Are there other manuals or
> tutorials I should try?

Both 'eval' and 'code_simp' use the code generator, which is why they're
described in the code generator manual, section 6.

Cheers
Lars




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