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
Thanks. Local_Theort.background_theory did the job.
This archive was generated by a fusion of
Pipermail (Mailman edition) and