[isabelle] Bug report: Locale parameters are not visible



The following theory does not verify. I consider this a bug of Isabelle 2009-2.

<<<<
theory test
  imports Main_ZF
begin

locale loc =
  fixes "x"

interpretation inter: loc "0" .

definition "a == inter.x"

end
>>>>

To work around of this it may be used:

<<<<
theory test
  imports Main_ZF
begin

locale loc =
  fixes "x"
begin

definition "x1 == x"

end

interpretation inter: loc "0" .

definition "a == inter.x1"

end
>>>>

Is it really a bug or just my misunderstanding of how Isabelle works? At least this is counter-intuitive.

-- 
Victor Porton - http://portonvictor.org





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