changeset 15647 | b1f486a9c56b |
parent 14516 | a183dec876ab |
child 17188 | a26a4fc323ed |
--- a/src/HOL/Import/HOL/num.imp Fri Apr 01 18:40:14 2005 +0200 +++ b/src/HOL/Import/HOL/num.imp Fri Apr 01 18:59:17 2005 +0200 @@ -12,7 +12,7 @@ thm_maps "NOT_SUC" > "Nat.nat.simps_1" "INV_SUC" > "Nat.Suc_inject" - "INDUCTION" > "List.lexn.induct" + "INDUCTION" > "NatArith.of_nat.induct" ignore_thms "num_TY_DEF"