Re: [isabelle] overloaded defs



Sean McLaughlin wrote:

Hello,

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

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"?

Thanks,

Sean

Maybe you just want the definition of this constant for these special types; the only way to do this right now in Isabelle is to scan through the axioms of a theory and look for something that looks like this definition.

Steven





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