Re: [isabelle] problem with local theories and the code generator



But then the code generator complains that "abs" is not a constant.
How can I solve this situation? It seems to me that I need either a)
jump away from a local_theory context for a while and let "abs" get
transformed to a real constant or b) I need something like a
"localized" code generator package.

Generally, you can try to work with general declarations with proper use
of morphisms, or make a reduced version that merely puts things into the
background theory context. For that you transform the abstract term once
to move it the global theory and then work with
Local_Theort.background_theory etc.

Thanks. Local_Theort.background_theory did the job.

Ondrej





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