summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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);