[Hol-info] Did anybody define "mod" or "gcd" in HOL?

[<li...@en...>]

Hi,

Did anybody define "mod" or "gcd" in HOL? And how to know where they are?

I found gcd has been defined in Isabelle/HOL, but I need in HOL4.  
Could anybody help me?

Best Wishes,
Liya