MAP_FIRST : ('a -> tactic) -> 'a list -> tactic
MAP_FIRST f [x1;...;xn] = (f x1) ORELSE ... ORELSE (f xn)
# needs "Library/floor.ml";;
# INTEGER_CLOSED;; val it : thm = |- (!n. integer (&n)) /\ (!x y. integer x /\ integer y ==> integer (x + y)) /\ (!x y. integer x /\ integer y ==> integer (x - y)) /\ (!x y. integer x /\ integer y ==> integer (x * y)) /\ (!x r. integer x ==> integer (x pow r)) /\ (!x. integer x ==> integer (--x)) /\ (!x. integer x ==> integer (abs x))
# g `integer(x) /\ integer(y) ==> integer(&2 * (x - &1) pow 7 + &11 * (y + &1))`;; ... # e(REPEAT STRIP_TAC);; val it : goalstack = 1 subgoal (1 total) 0 [`integer x`] 1 [`integer y`] `integer (&2 * (x - &1) pow 7 + &11 * (y + &1))`
# let INT_CLOSURE_TAC = MAP_FIRST MATCH_MP_TAC (CONJUNCTS(CONJUNCT2 INTEGER_CLOSED)) THEN TRY CONJ_TAC;;
e(REPEAT INT_CLOSURE_TAC THEN ASM_REWRITE_TAC[CONJUNCT1 INTEGER_CLOSED]);;