summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Fri, 22 Oct 1999 18:41:00 +0200 | |

changeset 7916 | 3cb310f40a3a |

parent 7915 | c7fd7eb3b0ef |

child 7917 | 5e5b9813cce7 |

replaced image_image_eq_UN by image_eq_UN

src/HOL/Fun.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Fun.ML Fri Oct 22 18:35:20 1999 +0200 +++ b/src/HOL/Fun.ML Fri Oct 22 18:41:00 1999 +0200 @@ -67,9 +67,9 @@ by (Blast_tac 1); qed "image_compose"; -Goal "f``g``A = (UN x:A. {f (g x)})"; +Goal "f``A = (UN x:A. {f x})"; by (Blast_tac 1); -qed "image_image_eq_UN"; +qed "image_eq_UN"; Goalw [o_def] "UNION A (g o f) = UNION (f``A) g"; by (Blast_tac 1);