Email Gateway (Aug 18 2022 at 13:25): Email Gateway (Aug 18 2022 at 13:25):From: Peter Lammich <peter.lammich@uni-muenster.de>
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
interpretation x: D
apply (unfold_locales)
apply simp
done
*** Duplicate fact "Scratch.x.A"
*** At command "done".
Many thanks for any hints,
Peter
Email Gateway (Aug 18 2022 at 13:25):From: Makarius <makarius@sketis.net>
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
Last updated: May 03 2024 at 04:19 UTC