`Isabelle's standard library has two different coercions from the
``naturals to
``the integers: IntDef.thy defines "int::nat=>int" which is
``monomorphic, and
`Nat.thy defines "of_nat::nat=>'a" which coerces from naturals into an

`arbitrary semiring. At type "nat=>int" they both mean exactly the
``same thing
``(see lemma IntDef.int_eq_of_nat). The only difference is that they
``are each
`set up with different sets of simp rules.

`My question is, why do we have both? If any of you have chosen to
``use one over
`the other, which one did you choose, and why?

`Unless there is a compelling reason to keep both, I would propose
``to either
``make "int" an abbreviation for "of_nat::nat=>int", or just
``eliminate it
``altogether. Also, if users prefer the way the simplifier works with
``"int",
`then the simp rules for "of_nat" should be changed accordingly.

`I could also ask the same thing about the overloaded function
``"real::'a=>real"
``from the HOL-Complex library, which is redundant with
``"of_nat::nat=>real" and
``"of_int::int=>real" at those types. Do we need separate constants
``for these?
`