Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Missing codegen theory

view this post on Zulip Email Gateway (Aug 19 2022 at 08:42):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Matthew,

there is now a whole bunch of examples in HOL/Predicate_Compile_Examples/.

Thanks for reporting this.

Florian
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 08:42):

From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Hi Florian,

Page 23 of the code generation tutorial [1] refers to a theory HOL/ex
/Predicate_Compile_ex.thy. I can't find this in the latest tarball. Is
it under a different name?

Thanks,
Matthew

[1]
http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/Isabelle2012/doc/codegen.pdf

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

Last updated: Nov 21 2024 at 12:39 UTC