Lines Matching defs:thms
68 val thms = [TIMES_2EXP1, arithmeticTheory.TIMES2, GSYM numeralTheory.iDUB]
69 val rwts = List.map (REWRITE_RULE thms)
351 val thms =
394 val thms =
396 mrw (GSYM bitTheory.MOD_2EXP_def)) thms
407 [computeLib.Defs thms,
1875 of SOME thms => MAP_EVERY ASSUME_TAC thms
2482 val thms = [WORD_ADD_LEFT_LO, WORD_ADD_LEFT_LS,
2490 map (Q.SPECL [`^n2w m`, `^n2w n`]) thms @