[isabelle-dev] Code generation in Isabelle

Alexander Krauss krauss at in.tum.de
Fri Jul 22 00:07:37 CEST 2011


On 07/21/2011 04:25 PM, Steven Obua wrote:
> Actually, there is a third code generator hidden somewhere in
> Isabelle.

If you are talking about what I know under the name "Compute Oracle", 
then rest assured that it is hidden well enough that the chance of some 
user accidentially confusing it with the mainstream code generator is 
negligible.

Interested parties can discover it using grep, of course.

Alex



More information about the isabelle-dev mailing list