| changeset 27213 | 2c7a628ccdcf |
| parent 27129 | 336807f865ce |
| child 27625 | 3a45b555001a |
--- a/src/HOL/Nat.thy Sat Jun 14 23:20:03 2008 +0200 +++ b/src/HOL/Nat.thy Sat Jun 14 23:20:05 2008 +0200 @@ -89,10 +89,6 @@ shows "P n" using assms by (rule nat.induct) -ML {* - fun nat_induct_tac n = res_inst_tac [("n", n)] @{thm nat_induct} -*} - declare nat.exhaust [case_names 0 Suc, cases type: nat] lemmas nat_rec_0 = nat.recs(1)