Fri, 23 Jun 2000 10:33:46 +0200 | paulson | added the allocator refinement proof | changeset | files |
Fri, 23 Jun 2000 10:33:11 +0200 | paulson | sum_below f n -> setsum f (lessThan n) | changeset | files |
Thu, 22 Jun 2000 23:04:34 +0200 | wenzelm | bind_thm(s); | changeset | files |