Lines Matching refs:res2
65 ``(by ==> R_ev (y,e,fns1,io1,ok1) res2) /\
70 (if isTrue ans1 then res2 else res3)``,
71 Q.SPEC_TAC (`res3`,`res3`) \\ Q.SPEC_TAC (`res2`,`res2`)
152 ``(b1 ==> R_ap (fc,FST res1,a,SND res1) res2) ==>
154 (b1 /\ b2 ==> R_ev (App fc el,a,fns,io,ok) res2)``,
155 Q.SPEC_TAC (`res2`,`res2`) \\ Q.SPEC_TAC (`res1`,`res1`)
377 (b2 ==> R_ev (e,FUNION (VarBind xs (FST res1)) a,SND res1) res2) ==>
379 R_ev (Let (ZIP (xs,ys)) e,a,fns,io,ok) res2``,
380 Q.SPEC_TAC (`res1`,`res1`) \\ Q.SPEC_TAC (`res2`,`res2`)