src/HOL/Probability/Bochner_Integration.thy
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
less more (0) -10 -2 tip