Re: [isabelle] overloaded defs

An overloaded constant simply refers to itself. There isn't a separate constant called "subset".


On 16 Feb 2006, at 14:37, Sean McLaughlin wrote:

  How do I find the actual constant an overloaded constant refers to?

read "(A::bool set) <= (B :: bool set)";
val it =
Const ("op <=", "bool set => bool set => bool") $ Free ("A", "bool set") $
      Free ("B", "bool set") : Term.term

How do I find that "op <=" means "subset"?

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