Lines Matching defs:first
205 fun first _ [] = raise ERR "first" "no items satisfy"
206 | first f (h::t) = if f h then h else first f t;
214 fun assoc x = snd o first (equal x o fst);
215 fun rev_assoc x = fst o first (equal x o snd);
419 fun find_redex r = first (fn rr as {redex, residue} => r = redex);
945 * first subgoal of tac1
954 => raise ERR "THEN1" "goal completely solved by first tactic"
971 * if the first conjunct is easily dispatched