src/HOL/UNITY/AllocBase.ML
changeset 9090 7141b912b0bb
parent 9026 640c4fd8b5b3
child 9107 67202a50ee6d
     1.1 --- a/src/HOL/UNITY/AllocBase.ML	Tue Jun 20 11:50:33 2000 +0200
     1.2 +++ b/src/HOL/UNITY/AllocBase.ML	Tue Jun 20 11:51:21 2000 +0200
     1.3 @@ -106,19 +106,17 @@
     1.4  by Auto_tac;
     1.5  qed "bag_of_sublist_lemma";
     1.6  
     1.7 -
     1.8  Goal "finite A \
     1.9  \     ==> bag_of (sublist l A) = \
    1.10  \         setsum (%i. if i < length l then {# nth l i #} else {#}) A";
    1.11  by (res_inst_tac [("xs","l")] rev_induct 1);
    1.12  by (Simp_tac 1);
    1.13  by (stac (symmetric Zero_def) 1);
    1.14 -by (etac (setsum_0 RS sym) 1);
    1.15 +by (rtac (setsum_0 RS sym) 1);
    1.16  by (asm_simp_tac (simpset() addsimps [sublist_append, 
    1.17  				      bag_of_sublist_lemma]) 1);
    1.18  qed "bag_of_sublist";
    1.19  
    1.20 -
    1.21  Goal "[| finite A; finite B |] \
    1.22  \     ==> bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = \
    1.23  \         bag_of (sublist l A) + bag_of (sublist l B)";