[isabelle] An induction rule

This seems like a really simple question, but after weeks of searching with no success I finally have to ask the list, since my student is waiting for the answer so he can finish his project: Where is (P(0) and (for all (j::nat > 0) there exists i < j such that (P(i) implies P(j)))) implies P(n) for all n? Many thanks! -WDMaurer
Prof. W. Douglas Maurer                Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University       Fax  (1-202)994-4875

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.