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 |
Fri, 16 Jun 2000 14:02:41 +0200 | paulson | real simprocs | changeset | files |
Fri, 16 Jun 2000 13:41:44 +0200 | paulson | fixed for removal of subset_empty | changeset | files |
Fri, 16 Jun 2000 13:39:21 +0200 | paulson | this proof needs more detail | changeset | files |
Fri, 16 Jun 2000 13:33:39 +0200 | paulson | uncommented the last 2 examples; tidied | changeset | files |
Fri, 16 Jun 2000 13:32:59 +0200 | paulson | new lemma real_minus_diff_eq | changeset | files |