Lines Matching refs:unfold
1375 Define `unfold proj f s =
1386 unfold proj f s =
1389 | SOME (s',l) => pcons (proj s) l (unfold proj f s')`,
1399 ((f x = NONE) ==> (unfold proj f x = stopped_at (proj x))) /\
1401 (unfold proj f x = pcons (proj x) v2 (unfold proj f v1)))`,
1408 `!proj f s. labels (unfold proj f s) = LUNFOLD f s`,
1434 okpath m (unfold proj f s)`,
1438 Q.EXISTS_TAC `\p. ?s. P s /\ (p = unfold proj f s)` THEN
1484 Q.EXISTS_TAC `unfold (��(s,tr). s)
1679 Q.EXISTS_TAC `unfold (��(p1,p2). (first p1, first p2))
1781 Q.EXISTS_TAC `unfold (��(p,t). t)