Dear Dr. Michael Norrish, Thank you so much! I have found them and learned the way to search such kind of theory.
I really appreciate your help! Best Wishes, Liya Quoting Michael Norrish <[email protected]>: > 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 > ------------------------------------------------------------------------------ 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
