[isabelle] Qualified name for Set.insert
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,
*** 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,
What is the reason for the qualified name not being defined, and is
there a better workaround?
This archive was generated by a fusion of
Pipermail (Mailman edition) and