Re: [isabelle-dev] Attributes and local theories

[Makarius]

On Mon, 14 Nov 2011, Andreas Schropp wrote:

But

  fun add_non_pervasive_declaration decl lthy =
     lthy
     |> Local_Theory.declaration false decl
     |> Context.proof_map (Morphism.form decl)

should do the job based on Isabelle2011-1's Local_Theory.declaration?

Yes, this is right.


        Makarius

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev