[isabelle-dev] Theory to Local Theory
makarius at sketis.net
Mon May 9 18:54:23 CEST 2011
On Mon, 9 May 2011, munddr at gmail.com wrote:
> I'm trying to convert a Theory to a Local Theory. I see that
> Local_Theory.exit_global converts a lthy to a thy, but is there a
> function for converting a thy to a lthy?
See Inductive.add_inductive_global (in ~~/src/HOL/Tools/inductive.ML) how
a local specification mechanism can be invoked within a old-style global
theory situation, using Named_Target.theory_init etc.
There are occasional good (historical) reasons for that, but the normal
way is to work with local_theory from the very start and let the system do
the init/exit wrapping.
More information about the isabelle-dev