src/HOL/List.ML
changeset 4132 daff3c9987cc
parent 4089 96fba19bcbe2
child 4423 a129b817b58a
     1.1 --- a/src/HOL/List.ML	Tue Nov 04 20:46:56 1997 +0100
     1.2 +++ b/src/HOL/List.ML	Tue Nov 04 20:47:38 1997 +0100
     1.3 @@ -713,6 +713,9 @@
     1.4  by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
     1.5  qed_spec_mp"set_take_whileD";
     1.6  
     1.7 +qed_goal "zip_Nil_Nil"   thy "zip []     []     = []" (K [Simp_tac 1]);
     1.8 +qed_goal "zip_Cons_Cons" thy "zip (x#xs) (y#ys) = (x,y)#zip xs ys" 
     1.9 +						      (K [Simp_tac 1]);
    1.10  (** replicate **)
    1.11  section "replicate";
    1.12