Re: [isabelle] Porting to 2009: Duplicate facts on locale interpretation



On Tue, 21 Apr 2009, Peter Lammich wrote:

I get a "duplicate fact"-error error when trying to interpret a locale
that imports a fact with the same name from different locales:
In Isabelle2007 this worked well, and I frequently use it. Do I have to
rename all those lemmas to make their names unique, or
is there a simpler way to convert ?

Here follows a toy-example that illustrates the problem:

 locale B =
   assumes Y: "True"
 begin
   lemma A: True ..
 end

 locale C =
   assumes Z: "True"
 begin
   lemma A: True ..
 end

 locale D = B + C
 begin
   lemma A: "True" ..
 end

Formerly there were more implicit (strange) prefixes in locale import expressions. Instead, the user can now add explicit qualifiers. For example, this is how to keep the name spaces of B and C separate in the merge:

  locale D = b: B + c: C
  begin
  ...


	Makarius





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