[isabelle] Qualified name for Set.insert



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





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