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

author | paulson |

Fri, 25 Aug 2000 12:15:35 +0200 | |

changeset 9687 | 772ac061bd76 |

parent 9686 | 87b460d72e80 |

child 9688 | d1415164b814 |

moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML

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

src/HOL/UNITY/Union.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Set.ML Thu Aug 24 12:39:42 2000 +0200 +++ b/src/HOL/Set.ML Fri Aug 25 12:15:35 2000 +0200 @@ -19,13 +19,13 @@ by (Asm_full_simp_tac 1); qed "CollectD"; -val [prem] = Goal "[| !!x. (x:A) = (x:B) |] ==> A = B"; +val [prem] = Goal "(!!x. (x:A) = (x:B)) ==> A = B"; by (rtac (prem RS ext RS arg_cong RS box_equals) 1); by (rtac Collect_mem_eq 1); by (rtac Collect_mem_eq 1); qed "set_ext"; -val [prem] = Goal "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}"; +val [prem] = Goal "(!!x. P(x)=Q(x)) ==> {x. P(x)} = {x. Q(x)}"; by (rtac (prem RS ext RS arg_cong) 1); qed "Collect_cong"; @@ -557,6 +557,7 @@ \ (UN x:A. C(x)) = (UN x:B. D(x))"; by (asm_simp_tac (simpset() addsimps prems) 1); qed "UN_cong"; +Addcongs [UN_cong]; section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)"; @@ -591,6 +592,7 @@ \ (INT x:A. C(x)) = (INT x:B. D(x))"; by (asm_simp_tac (simpset() addsimps prems) 1); qed "INT_cong"; +Addcongs [INT_cong]; section "Union";