# HG changeset patch # User nipkow # Date 951378996 -3600 # Node ID ebf874fcbff2814549cfc8454ca9ad0888285a19 # Parent 42911a6bb13f4c5757f71310614a392ee87e8960 renamed a lemma diff -r 42911a6bb13f -r ebf874fcbff2 src/HOL/BCV/Orders.ML --- a/src/HOL/BCV/Orders.ML Thu Feb 24 08:55:37 2000 +0100 +++ b/src/HOL/BCV/Orders.ML Thu Feb 24 08:56:36 2000 +0100 @@ -147,7 +147,7 @@ Goalw [listsn_def] "[| xs : listsn n A; x:A; i < n |] ==> xs[i := x] : listsn n A"; by (Asm_full_simp_tac 1); -by (blast_tac (claset() addDs [set_list_update_subset RS subsetD]) 1); +by (blast_tac (claset() addDs [set_update_subset_insert RS subsetD]) 1); qed "list_update_in_listsn"; Addsimps [list_update_in_listsn]; AddSIs [list_update_in_listsn]; diff -r 42911a6bb13f -r ebf874fcbff2 src/HOL/MicroJava/BV/Correct.ML --- a/src/HOL/MicroJava/BV/Correct.ML Thu Feb 24 08:55:37 2000 +0100 +++ b/src/HOL/MicroJava/BV/Correct.ML Thu Feb 24 08:56:36 2000 +0100 @@ -114,7 +114,7 @@ Goalw [approx_loc_def,list_all2_def] "\\loc idx x X. (approx_loc G hp loc LT) \\ (approx_val G hp x X) \ \ \\ (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"; -by (fast_tac (claset() addDs [set_update_subset RS subsetD] +by (fast_tac (claset() addDs [set_update_subset_insert RS subsetD] addss (simpset() addsimps [zip_update])) 1); qed_spec_mp "approx_loc_imp_approx_loc_subst";