Fri, 05 Mar 2010 09:09:11 -0800 | huffman | skip proof of induction rule for indirect-recursive domain definitions | changeset | files |
Fri, 05 Mar 2010 17:49:10 +0100 | hoelzl | generalized inj_uminus; added strict_mono_imp_inj_on | changeset | files |
Fri, 05 Mar 2010 10:42:13 +0100 | hoelzl | merged | changeset | files |
Thu, 04 Mar 2010 21:52:26 +0100 | hoelzl | Add Lebesgue integral and probability space. | changeset | files |
Thu, 04 Mar 2010 19:50:45 +0100 | hoelzl | Supremum and Infimum on real intervals | changeset | files |
Thu, 04 Mar 2010 19:43:51 +0100 | hoelzl | Rewrite rules for images of minus of intervals | changeset | files |
Thu, 04 Mar 2010 18:42:39 +0100 | hoelzl | Add dense_le, dense_le_bounded, field_le_mult_one_interval. | changeset | files |