# Re: [isabelle] overloaded defs

Steven Obua wrote:

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

I have some code to do this sort of thing.
tc["op <="];
val it =
[(["Finite_Set.min_max.below_inf_sup_Inf_Sup.ACIfSL_inf"],
"ACIfSL min op <="),
(["Orderings.order_class.order_refl",
"Orderings.order_class.axioms_1"],
"?x <= ?x"),
(etc)
filrpm "a <= b == x" it;
val it =
[(["Nat.le_def"], "?m <= ?n == ~ ?n < ?m"),
(["Set.subset_def"], "?A <= ?B == ALL x:?A. x : ?B"),
(["IntDef.le_int_def"],
"?z <= ?w ==
EX x y u v.
x + v <= u + y &
(x, y) : Rep_Integ ?z & (u, v) : Rep_Integ ?w")]
: (string list * Thm.thm) list
It's in
http://users.rsise.anu.edu.au/~jeremy/isabelle/gen05/gen.ML
Jeremy

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