Minor changes due to primrec definition for nth
authorpusch
Thu, 06 Mar 1997 16:05:32 +0100
changeset 2739 5481b1c73d84
parent 2738 e28a0668dbfe
child 2740 2c549ae2563b
Minor changes due to primrec definition for nth
src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Mar 06 16:04:23 1997 +0100
+++ b/src/HOL/List.ML	Thu Mar 06 16:05:32 1997 +0100
@@ -288,11 +288,6 @@
 
 (** nth **)
 
-val [nth_0,nth_Suc] = nat_recs nth_def; 
-store_thm("nth_0",nth_0);
-store_thm("nth_Suc",nth_Suc);
-Addsimps [nth_0,nth_Suc];
-
 goal List.thy
   "!xs. nth n (xs@ys) = \
 \          (if n < length xs then nth n xs else nth (n - length xs) ys)";