```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.