src/HOL/Product_Type.thy
changeset 45607 16b4f5774621
parent 45205 2825ce94fd4d
child 45662 4f7c05990420
     1.1 --- a/src/HOL/Product_Type.thy	Sun Nov 20 21:07:06 2011 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Sun Nov 20 21:07:10 2011 +0100
     1.3 @@ -625,7 +625,7 @@
     1.4    Setup of internal @{text split_rule}.
     1.5  *}
     1.6  
     1.7 -lemmas prod_caseI = prod.cases [THEN iffD2, standard]
     1.8 +lemmas prod_caseI = prod.cases [THEN iffD2]
     1.9  
    1.10  lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
    1.11    by (fact splitI2)