Lines Matching refs:word
257 val sw2sw_ss = eval_term_ss "sw2sw" ``(sw2sw:'a word->'b word) (n2w n)``
258 val w2w_ss = eval_term_ss "w2w" ``(w2w:'a word->'b word) (n2w n)``
511 ``(n2w n ?? n2w m):('a word)``,``(n2w n || n2w m):('a word)``,``(n2w n && n2w m):('a word)``,
512 ``(n2w n + n2w m):('a word)``, ``(n2w n - n2w m):('a word)``, ``(n2w n * n2w m):('a word)``,
513 ``n2w n < (n2w m):('a word)``, ``n2w n <= (n2w m):('a word)``, ``n2w n > (n2w m):('a word)``, ``n2w n >= (n2w m):('a word)``,
514 ``n2w n <+ (n2w m):('a word)``, ``n2w n <=+ (n2w m):('a word)``, ``n2w n >+ (n2w m):('a word)``, ``n2w n >=+ (n2w m):('a word)``,
515 ``(n2w n):('a word) << m``, ``(n2w n):('a word) >> m``, ``(n2w n):('a word) >>> m``, ``~(n2w n):('a word)``,
516 ``w2n ((n2w n):'a word)``];
1105 else if can (match_term ``p + n2w n:'a word``) x then
1107 else if can (match_term ``p - n2w n:'a word``) x then