src/HOL/BCV/Orders.ML
changeset 8288 ebf874fcbff2
parent 7961 422ac6888c7f
child 8423 3c19160b6432
equal deleted inserted replaced
8287:42911a6bb13f 8288:ebf874fcbff2
   145 qed "listsnE_nth_in";
   145 qed "listsnE_nth_in";
   146 
   146 
   147 Goalw [listsn_def]
   147 Goalw [listsn_def]
   148  "[| xs : listsn n A; x:A; i < n |] ==> xs[i := x] : listsn n A";
   148  "[| xs : listsn n A; x:A; i < n |] ==> xs[i := x] : listsn n A";
   149 by (Asm_full_simp_tac 1);
   149 by (Asm_full_simp_tac 1);
   150 by (blast_tac (claset() addDs [set_list_update_subset RS subsetD]) 1);
   150 by (blast_tac (claset() addDs [set_update_subset_insert RS subsetD]) 1);
   151 qed "list_update_in_listsn";
   151 qed "list_update_in_listsn";
   152 Addsimps [list_update_in_listsn];
   152 Addsimps [list_update_in_listsn];
   153 AddSIs [list_update_in_listsn];
   153 AddSIs [list_update_in_listsn];
   154 
   154 
   155 
   155