src/HOL/Probability/Caratheodory.thy
changeset 37591 d3daea901123
parent 37032 58a0757031dd
child 38656 d5d342611edb
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Mon Jun 28 15:03:07 2010 +0200
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Mon Jun 28 15:03:07 2010 +0200
     1.3 @@ -829,7 +829,7 @@
     1.4          with sbBB [of i] obtain j where "x \<in> BB i j"
     1.5            by blast        
     1.6          thus "\<exists>i. x \<in> split BB (prod_decode i)"
     1.7 -          by (metis prod_encode_inverse prod.cases prod_case_split)
     1.8 +          by (metis prod_encode_inverse prod.cases)
     1.9        qed 
    1.10      have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
    1.11        by (rule ext)  (auto simp add: C_def)