# HG changeset patch
# User wenzelm
# Date 1213478405 -7200
# Node ID 2c7a628ccdcfa83afab58d4d2f450d9c1e509b7a
# Parent  3a3686dd4433c09cc76ab216ec7fc18ae401cdbe
removed obsolete nat_induct_tac -- cannot work without;

diff -r 3a3686dd4433 -r 2c7a628ccdcf src/HOL/Nat.thy
--- 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)