Email Gateway (Aug 18 2022 at 13:51): Email Gateway (Aug 18 2022 at 13:51):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
I just wondered that the constant insert (defined in Set.thy) is not
accessible via the qualified name "Set.insert".
I have a locale that defines an insert-constant itself, and tried to use
Set.insert to access the original constant. However,
Isabelle sais:
*** No such constant: "Set.insert"
*** At command "lemma".
My current workaround is to define an abbreviation "set_insert ==
insert" before I re-define the constant or rename my own constant to,
e.g. "insrt".
What is the reason for the qualified name not being defined, and is
there a better workaround?
Many thanks,
Peter
Last updated: May 03 2024 at 08:18 UTC