summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Tue, 10 Feb 2009 09:46:11 +0000 | |

changeset 29852 | 3d4c46f62937 |

parent 29836 | 3d935e8b0bf7 |

child 29853 | e2103746a85d |

Deleted the induction rule nat_induct2, which was too weak and not used even once.

src/HOL/Nat.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Nat.thy Mon Feb 09 11:15:13 2009 +0000 +++ b/src/HOL/Nat.thy Tue Feb 10 09:46:11 2009 +0000 @@ -846,13 +846,6 @@ thus "P i j" by (simp add: j) qed -lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n" - apply (rule nat_less_induct) - apply (case_tac n) - apply (case_tac [2] nat) - apply (blast intro: less_trans)+ - done - text {* The method of infinite descent, frequently used in number theory. Provided by Roelof Oosterhuis. $P(n)$ is true for all $n\in\mathbb{N}$ if