# HG changeset patch # User pusch # Date 857660732 -3600 # Node ID 5481b1c73d841ce249061d875ce9b6ae6e1499e4 # Parent e28a0668dbfe4fcc719c773604dbdd37e9a3d60c Minor changes due to primrec definition for nth diff -r e28a0668dbfe -r 5481b1c73d84 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)";