removed obsolete nat_induct_tac -- cannot work without;
authorwenzelm
Sat Jun 14 23:20:05 2008 +0200 (2008-06-14)
changeset 272132c7a628ccdcf
parent 27212 3a3686dd4433
child 27214 0978b8e32fd0
removed obsolete nat_induct_tac -- cannot work without;
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Sat Jun 14 23:20:03 2008 +0200
     1.2 +++ b/src/HOL/Nat.thy	Sat Jun 14 23:20:05 2008 +0200
     1.3 @@ -89,10 +89,6 @@
     1.4    shows "P n"
     1.5    using assms by (rule nat.induct) 
     1.6  
     1.7 -ML {*
     1.8 -  fun nat_induct_tac n = res_inst_tac [("n", n)] @{thm nat_induct}
     1.9 -*}
    1.10 -
    1.11  declare nat.exhaust [case_names 0 Suc, cases type: nat]
    1.12  
    1.13  lemmas nat_rec_0 = nat.recs(1)