Lines Matching defs:x2
33 (SEP_EXISTS x1 x2 x3 x4.
35 (HD (xs ++ Sym "NIL"::stack),x1,x2,x3,x4,bc_state_tree bc,
58 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x2`
107 val (x2,s2) = pred_setSyntax.dest_insert s1
108 in ISPECL [x1,x2,s2] INSERT_COMM end
164 (SPEC_EX `arg2` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4`
167 (SPEC_EX `Sym "NIL"` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4`
172 (SPEC_EX `NFIX arg2` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4`
182 (SPEC_EX `NFIX arg1` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4`
185 (SPEC_EX `NFIX arg2` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4`
189 (SPEC_EX `x1` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4`
193 (SPEC_EX `x1` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4`
197 (SPEC_EX `x1` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4`
201 (SPEC_EX `x1` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4`
205 (SPEC_EX `x1` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4`
306 (x0,x1,x2,x3,x4,x5,xs,io,xbp,qs,code,amnt) * ~zS`
433 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x2`
585 STRIP_TAC \\ `?x1 x2 x3 x4 x5. x = (x1,x2,x3,x4,x5)` by METIS_TAC [PAIR]
1164 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x2`
1203 val th = th |> Q.GEN `x4` |> Q.GEN `x3` |> Q.GEN `x2` |> Q.GEN `x1`
1363 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x2`
1387 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x2`