Tue, 20 Jun 2000 11:42:24 +0200 | paulson | replaced the useless [p]subset_insertD by [p]subset_insert_iff | changeset | files |
Tue, 20 Jun 2000 11:41:25 +0200 | paulson | now setsum f A = 0 unless A is finite | changeset | files |
Tue, 20 Jun 2000 11:41:07 +0200 | paulson | now setsum f A = 0 unless A is finite; proved setsum_cong | changeset | files |