I'm not sure how much this experience is worth, because it is such a different environment than the standard college proof environment, but the high school math program PROMYS does this. I believe Ross, which an older program that PROMYS is strongly influenced by, uses the same model.
More precisely, in the first two weeks of PROMYS, students are challenged to prove statements about integers and allowed to keep a list of what axioms they choose to use. In the second week, we start discussions about which axioms might be redundant or better in one way or another. (The statement $x \times 0 = 0$ is on a lot of axiom lists at first, but is eventually realized to follow from the other ring properties.) By the end of the second week, we converge to the standard PROMYS axioms of $\mathbb{Z}$ which are:
$\mathbb{Z}$ is a commutative ordered ring, and every nonempty set of positive integers has a least element.
Here are some problems which occur during the first two weeks, and are substantially easier with strong than weak induction:
If $x$ and $y$ are positive integers and $x|y$, then $x \leq y$.
If $a$ is an integer and $b$ a positive integer, there exist integers $q$ and $r$, with $0 \leq r < b$, such that $a = qb+r$.
Every integer $\geq 2$ is divisible by a prime.
Every integer $\geq 2$ can be written as a product of primes.
If $a$ and $b$ are integers, then there are integers $x$ and $y$ such that $ax+by$ divides $a$ and divides $b$.
We always get a number of students who have already seen standard induction in high school, so I got used to (a) showing how to deduce strong induction from standard induction and (b) showing how strong induction proofs of the above statements were nicer to write than standard ones. I also think that PROMYS made a good choice in choosing the phrasing:
Every nonempty subset of positive integers has a least element.
rather than
If you can prove the implication $\forall_{m <n} S(m) \implies S(n)$ then you can prove $\forall_n S(n)$.
They are logically the same, but I think that thinking about manipulating statements $S( \ )$ like that is confusing. In the comments below, katz points out that there are two differences between the statements: I have switched from first order to second order logic, as well as taking the contrapositive. See the discussion below.
However, I would caution that these are really smart and dedicated kids, so they probably aren't a good model for a college class.