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

[Michael N. <Mic...@ni...>]

On 29/06/10 06:41, li...@en... wrote:
> 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?

MOD is in arithmeticTheory.

gcd is in gcdTheory.

If all else fails, commands like

   grep -R --include *Script.sml -i gcd *

will often lead you to the answer.

(Assuming you're on a Unix-like system with grep installed...)

Michael