| Fri, 09 Nov 2012 14:14:45 +0100 | immler | removed redundant/unnecessary assumptions from projective_family | changeset | files |
| Wed, 07 Nov 2012 14:41:49 +0100 | immler | assume probability spaces; allow empty index set | changeset | files |
| Wed, 07 Nov 2012 11:33:27 +0100 | immler | added projective_family; generalized generator in product_prob_space to projective_family | changeset | files |
| Tue, 06 Nov 2012 11:03:28 +0100 | immler | moved lemmas further up | changeset | files |
| Thu, 08 Nov 2012 20:02:41 +0100 | bulwahn | tuned proofs | changeset | files |
| Thu, 08 Nov 2012 19:55:37 +0100 | bulwahn | using hyp_subst_tac that allows to pass the current simpset to avoid the renamed bound variable warning in the simplifier | changeset | files |