[isabelle] Session with more than one parent



Hi Isabelle folk,

As far as I'm aware, a session can only have a single parent:

    session my_session = parent +
      ...

Sometimes I want to build on top of two previous sessions. The syntax makes it tempting to write:

    session my_session = parent1 + parent2 +
      ...

However, this is invalid. So I typically achieve what I want with an intermediate base session:

    session intermediate = parent1 +
      ... (* definition of parent2 repeated *)

    session my_session = intermediate +
      ...

This works, but if theories in 'parent2' change, I end up effectively rebuilding its heap image
twice. Also, if someone changes the definition of 'parent2' and I fail to notice and update my
corresponding definition of 'intermediate' unexpected things may happen in future.

Is there a way to achieve this without an intermediate session? Failing that, is there a more robust
way to specify this intermediate session? It's possible I'm just not being creative enough in how
I'm choosing to define these sessions.

Thanks for your time,
Matthew

________________________________

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.