src/HOL/List.ML

--- a/src/HOL/List.ML	Wed Jun 24 11:24:52 1998 +0200
+++ b/src/HOL/List.ML	Wed Jun 24 13:59:45 1998 +0200
@@ -537,6 +537,18 @@
 qed_spec_mp "nth_mem";
 Addsimps [nth_mem];
 
+(** list update **)
+
+section "list update";
+
+Goal "!i. length(xs[i:=x]) = length xs";
+by (induct_tac "xs" 1);
+by (Simp_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [split_nat_case]) 1);
+qed_spec_mp "length_list_update";
+Addsimps [length_list_update];
+
+
 (** last & butlast **)
 
 Goal "last(xs@[x]) = x";