| Fri, 26 Aug 2011 15:11:26 -0700 | huffman | NEWS entry for setsum_norm ~> norm_setsum | changeset | files |
| Fri, 26 Aug 2011 15:00:00 -0700 | huffman | make HOL-Probability respect set/pred distinction | changeset | files |
| Fri, 26 Aug 2011 23:14:36 +0200 | wenzelm | merged | changeset | files |
| Wed, 08 Sep 2010 16:10:49 -0700 | huffman | use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names) | changeset | files |
| Fri, 26 Aug 2011 10:38:29 -0700 | huffman | merged | changeset | files |
| Fri, 26 Aug 2011 08:56:29 -0700 | huffman | generalize and simplify proof of continuous_within_sequentially | changeset | files |
| Fri, 26 Aug 2011 08:12:38 -0700 | huffman | add lemma sequentially_imp_eventually_within; | changeset | files |