# HG changeset patch
# User nipkow
# Date 951378937 -3600
# Node ID 42911a6bb13f4c5757f71310614a392ee87e8960
# Parent  d4b895d3afa797b48884f77a2791ae8fd63c6f99
Added and renamed a lemma.

diff -r d4b895d3afa7 -r 42911a6bb13f src/HOL/List.ML
--- a/src/HOL/List.ML	Wed Feb 23 10:45:08 2000 +0100
+++ b/src/HOL/List.ML	Thu Feb 24 08:55:37 2000 +0100
@@ -485,13 +485,6 @@
 qed "set_upt";
 Addsimps [set_upt];
 
-Goal "!i < size xs. set(xs[i := x]) <= insert x (set xs)";
-by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
-by (Blast_tac 1);
-qed_spec_mp "set_list_update_subset";
-
 Goal "(x : set xs) = (? ys zs. xs = ys@x#zs)";
 by (induct_tac "xs" 1);
  by (Simp_tac 1);
@@ -744,8 +737,11 @@
  by (asm_full_simp_tac (simpset() addsimps []) 1);
 by (asm_full_simp_tac (simpset() addsplits [nat.split]) 1);
 by (Fast_tac  1);
-qed_spec_mp "set_update_subset";
+qed_spec_mp "set_update_subset_insert";
 
+Goal "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A";
+by(fast_tac (claset() addSDs [set_update_subset_insert RS subsetD]) 1);
+qed "set_update_subsetI";
 
 (** last & butlast **)