[isabelle] Locales: Interpretation changes behaviour of locale expression



Hi,

I ran into the following unexpected behaviour with locales:

theory Scratch
imports Main
begin

  locale A begin
    definition "name â True"
  end

  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*)
  
end


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?

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

--
  Peter








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