[isabelle] correct Isabelle/ML idiom for parsing assumption for new locale



I want to embed a locale L2 within L1.  L1 has a local constant called c, and the user's assumption I'm parsing includes references to c.

At the Isabelle/ML level, I therefore have code that looks like

   val lthy = Named_Target.init L1name thy
   val asm = Syntax.read_term lthy user_string
   val e = Element.Assumes [((L2name, []), [(@{term "Trueprop"} $ asm, [])])]

This seems to correctly handle the user's "c" as a reference to constant c, but then I need to create L2, and trying with

   Expression.add_locale L2name L2name L1expr [e] thy

seems to reinterpret the c in e as something that needs universal quantification rather than as a reference to L1's constant.

So, what's the right way to do this?

Michael



________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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