Lines Matching refs:xx
553 ``!x1 a. ~(xx IN b) /\ ~(xx - 4w IN b) ==>
554 (lisp_x x1 (a,b,(xx =+ x) f) s = lisp_x x1 (a,b,f) s)``,
557 \\ `~(xx = a)` by METIS_TAC []
559 \\ `~(a = xx - 4w)` by METIS_TAC []
567 \\ Q.PAT_ABBREV_TAC `xx = a - n2w n`
568 \\ `~(xx IN bb) /\ ~(xx - 4w IN bb)` by
569 (Q.UNABBREV_TAC `bb` \\ Q.UNABBREV_TAC `xx`
583 (Q.UNABBREV_TAC `xx`
677 \\ REPEAT (Q.PAT_X_ASSUM `!xx yy. bb` (K ALL_TAC))
710 (RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `f5 xx = yy` (fn th => REWRITE_TAC [GSYM th]))