On 29/06/10 06:41, [email protected] 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 ------------------------------------------------------------------------------ This SF.net email is sponsored by Sprint What will you do first with EVO, the first 4G phone? Visit sprint.com/first -- http://p.sf.net/sfu/sprint-com-first _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
