[isabelle-dev] Theory to Local Theory

[Makarius]

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.


 	Makarius