Lines Matching defs:cm
233 val cm = List.nth(uargs,2)
284 ``assert_mode ^cm``,
292 SPECL [``16w:bool[5]``, cm] comb_mode_thm] a_thm
302 val cm' = (same_const opr ``write_cpsr``);
304 if (cm')
306 ``^cm:bool[5]``
434 val cm = List.nth(uargs,2)
509 THEN ASSUME_TAC (SPECL [!global_mode, cm] comb_mode_thm)
510 THEN ASSUME_TAC (SPECL [src_inv,``(assert_mode ^cm)``,
516 ASSUME_TAC (SPECL [``16w:bool[5]``,cm] comb_mode_thm)
518 (SPECL [src_inv,``(assert_mode ^cm)``,
523 THEN ASSUME_TAC (SPECL [l,r, ``16w:bool[5]``, cm,
566 val cm = List.nth(uargs,2)