Lines Matching refs:res2
33 let (res2,s2) = sem env' (s' with clock := i') e' in
34 case (res1, res2) of
149 Cases_on `res2` >>
233 `?s2 res2. sem env (s with clock := i') e1 = (res2,s2)` by metis_tac [pair_CASES] >>
235 reverse (Cases_on `res2`) >>
240 `?s2' res2'. sem env' (s' with clock := i') e1' = (res2',s2')` by metis_tac [pair_CASES] >>
242 >- (Cases_on `res2'` >>
245 Cases_on `res2'` >>