author | pusch |
Thu, 06 Mar 1997 16:05:32 +0100 | |
changeset 2739 | 5481b1c73d84 |
parent 2738 | e28a0668dbfe |
child 2740 | 2c549ae2563b |
src/HOL/List.ML | file | annotate | diff | comparison | revisions |
--- 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)";