Re: [isabelle] overloaded defs
Sean McLaughlin wrote:
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
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
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