src/HOL/List.ML
changeset 6451 bc943acc5fda
parent 6433 228237ec56e5
child 6794 ac367328b875
     1.1 --- a/src/HOL/List.ML	Mon Apr 19 17:53:38 1999 +0200
     1.2 +++ b/src/HOL/List.ML	Tue Apr 20 14:32:48 1999 +0200
     1.3 @@ -333,13 +333,11 @@
     1.4  qed "rev_map";
     1.5  
     1.6  (* a congruence rule for map: *)
     1.7 -Goal "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
     1.8 -by (rtac impI 1);
     1.9 +Goal "xs=ys ==> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
    1.10  by (hyp_subst_tac 1);
    1.11  by (induct_tac "ys" 1);
    1.12  by Auto_tac;
    1.13 -val lemma = result();
    1.14 -bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
    1.15 +bind_thm("map_cong", impI RSN (2,allI RSN (2, result() RS mp)));
    1.16  
    1.17  Goal "(map f xs = []) = (xs = [])";
    1.18  by (induct_tac "xs" 1);