Lines Matching refs:word
193 (``words$word_mod:'a word -> 'a word -> 'a word``, 2,
451 fcp_eq_thm : generates a bitwise equality theorem for a given word type.
458 ���!a b:'a word.
521 (SPECL [���w: 'a word���, ���arithmetic$NUMERAL a���] WORD_MUL_LSL))
570 SPECL [���a: 'a words$word���, ���n2w (NUMERAL n) : 'a word���]
612 ���!l h n w:'a word.
618 ���!l h n w:'a word.
779 ``(if b then x:'a word else y) ' i = if b then x ' i else y ' i``
786 ���INT_MINw :'a word = FCP i. i = dimindex (:'a) - 1���,
790 ���-1w : 'a word = $FCP (K T)���,
794 ���!w: 'a word. w2w w : 'b word = FCP i. i < dimindex (:'a) /\ w ' i���,
798 ���!w: 'a word.
799 sw2sw w :'b word =
838 (``words$word_2comp:'a word -> 'a word``, 1, WORD_NEG_CONV),
839 (``words$word_mul:'a word -> 'a word -> 'a word``, 2, BLAST_MUL_CONV),
840 (``words$word_lsl_bv:'a word -> 'a word -> 'a word``, 2, LSL_BV_CONV),
841 (``words$word_lsr_bv:'a word -> 'a word -> 'a word``, 2, LSR_BV_CONV),
842 (``words$word_asr_bv:'a word -> 'a word -> 'a word``, 2, ASR_BV_CONV),
843 (``words$word_ror_bv:'a word -> 'a word -> 'a word``, 2, ROR_BV_CONV),
844 (``words$word_rol_bv:'a word -> 'a word -> 'a word``, 2, ROL_BV_CONV)
1057 ���!i a b:'a word.
1071 val () = if tr then print ("Checking " ^ toString n ^ " bit word\n")