[isabelle] Locales: Interpretation changes behaviour of locale expression


I ran into the following unexpected behaviour with locales:

theory Scratch
imports Main

  locale A begin
    definition "name â True"

  interpretation foo!: A by (unfold_locales)  (* If this line is
removed, everything works as expected. *)

  locale B = A +
    assumes "name"  (* Name is a FREE VARIABLE here*)

When defining locale B, I would have expected "name" to reference to the
definition in A. However, if there is an interpretation of A before,
"name" is a free variable in the definition of B, and I have no idea how
to access "name" from A?

  1. Is this the correct behaviour?
  2. How to correctly reference "name" from A, in the definition of B?


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