# HG changeset patch # User paulson # Date 1031756039 -7200 # Node ID 40e4755e57f7c54b673eea6cf5f7c6ed01699c41 # Parent 1500a2e48d443d3c27e6e386a0ab01f913df3228 Bound variable preservation in Collect_cong diff -r 1500a2e48d44 -r 40e4755e57f7 src/ZF/ZF.ML --- a/src/ZF/ZF.ML Tue Sep 10 16:51:31 2002 +0200 +++ b/src/ZF/ZF.ML Wed Sep 11 16:53:59 2002 +0200 @@ -321,7 +321,8 @@ qed "CollectD2"; val prems= Goalw [Collect_def] - "[| A=B; !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)"; + "[| A=B; !!x. x:B ==> P(x) <-> Q(x) |] \ +\ ==> Collect(A, %x. P(x)) = Collect(B, %x. Q(x))"; by (simp_tac (simpset() addsimps prems) 1) ; qed "Collect_cong";